Fundamental Constructs

Expressions

Expressions in Disp are programs and match the untyped lambda calculus. They are represented as follows:

#![allow(unused)]
fn main() {
enum Expr {
	Var,
	Lam { bind: Binding, expr: Expr },
	App { func: Expr, func: Expr },
}
enum Binding {
	None,
	End,
	Branch(Binding, Binding),
}
}

See how the Binding structure works here.

Judgements

#![allow(unused)]
fn main() {
struct Judgement {
	term: Expr,
	ty: Expr,
}
}

Judgements are considered valid if when the structure of term is encoded into the lambda calculus, and Expr::App(ty, encoding) beta-reduces to Expr::Var.

Contexts

#![allow(unused)]
fn main() {
struct Context {
	names: Map<String, Judgement>
}
}