A small dependently typed language

Extends elab-dependent.

This is a variant of the elab-dependent project with fancier syntactic sugar for functions and let bindings. See that project’s README for more details and resources.

Example

let Bool := fun (Out : Type) (true : Out) (false : Out) -> Out;
let true : Bool := fun Out true false => true;
let false : Bool := fun Out true false => false;

let not (b : Bool) : Bool :=
  fun (Out : Type) (true : Out) (false : Out) => b Out false true;

true Bool false

$ cat ./test/readme/bools.txt | dependent-sugar norm
<input> :
  fun (false : fun (Out : Type) (true : Out) (false : Out) -> Out)
      (Out : Type) (true : Out) (false : Out) -> Out
:= fun false Out true false => false