def check (ctx : TypeCtx) (t : Term) : Option CurryType

Type assignment checker Returns some ty if t can be assigned type ty in context ctx, or none if the term is ill-typed.

• .var c: look up c in the context.
• .abs x m: check m, look up x's type, and form the arrow type x.ty → m.ty.
• .app m n: check both m and n; require m : domain → ty and n : domain.

Equations

• One or more equations did not get rendered due to their size.
• check ctx (Term.var c) = ctx.lookup c
• check ctx (Term.abs x m) = match check ctx m with | none => none | some ty => match ctx.lookup x with | none => none | some ty' => some (ty'.arrow ty)

def WellTyped (ctx : TypeCtx) (t : Term) (ty : CurryType) : Prop

Predicate asserting that term t has type ty in context ctx. Defined as the decidable proposition check ctx t = some ty.

Equations

• WellTyped ctx t ty = (check ctx t = some ty)

def runTest' (name : String) (t : Term) : String

Equations

• One or more equations did not get rendered due to their size.