Skip to content

Instantly share code, notes, and snippets.

@qexat

qexat/levelled_term.v

Created May 12, 2025 15:36
Show Gist options
  • Save qexat/8a6494b2c3d4e424e4680dd891c7d515 to your computer and use it in GitHub Desktop.
Save qexat/8a6494b2c3d4e424e4680dd891c7d515 to your computer and use it in GitHub Desktop.
Download ZIP
levelled term using a GADT (rocq)
Raw
levelled_term.v
Require Import String.
Inductive Term : nat -> Type :=
| App : forall {n m : nat}, Term (S n) -> Term m -> Term (n + m)
| Fun : forall {n : nat}, Term 0 -> Term n -> Term (S n)
| Var : string -> Term 0.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment