ctx

Documentation

Index

• type Binding
• type Ctx
  • func (c Ctx) Drop() Ctx
  • func (c *Ctx) Extend(name string, ty ast.Term)
  • func (c Ctx) Len() int
  • func (c Ctx) LookupVar(ix int) (ast.Term, bool)

Types

type Binding

type Binding struct {
	Name string
	Ty   ast.Term
}

Binding represents a binding in the context.

type Ctx

type Ctx struct {
	Tele []Binding
}

Ctx represents the typing context.

func (Ctx) Drop

func (c Ctx) Drop() Ctx

Drop removes the most recent binding from the context.

func (*Ctx) Extend

func (c *Ctx) Extend(name string, ty ast.Term)

Extend adds a new binding to the context.

func (Ctx) Len

func (c Ctx) Len() int

Len returns the length of the context.

func (Ctx) LookupVar

func (c Ctx) LookupVar(ix int) (ast.Term, bool)

LookupVar looks up the type of a de Bruijn variable. ix=0 is the most recent binding.