Skip to content

Instantly share code, notes, and snippets.

@jkoppel

jkoppel/Lang.v

Created April 9, 2020 16:30
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jkoppel/2cb6a49d4dab41e0ed28c81983bc1df7 to your computer and use it in GitHub Desktop.
Save jkoppel/2cb6a49d4dab41e0ed28c81983bc1df7 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Lang.v
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