Skip to content

Instantly share code, notes, and snippets.

@jkoppel
Created Apr 9, 2020
Embed
What would you like to do?
Inductive val :=
| ValConst (n : nat)
| Closure (e1 : list val) (e2 : exp)
with
exp :=
| Var (v : var)
| Plus (e1 e2 : exp)
| App (e1 e2 : exp)
| Const (n : nat)
| Lambda (e : exp)
| Clo (e1 : list val) (e2 : exp)
| Assert (e : exp) (p : nat -> Type)
.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment