syntaxAlchemist/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

add notation for debruijn terms

Browse source
This commit is contained in:
Michael Sippel 2024-09-20 19:53:27 +02:00
parent c4f4e56fee
commit f174eb1061
1 changed files with 56 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

57
coq/terms_debruijn.v
View file

@ -27,11 +27,66 @@ Inductive expr_DeBruijn : Type :=
| ex_abs : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
| ex_morph : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
| ex_app : expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
| ex_let : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
| ex_let : expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
| ex_ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
| ex_descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
.
Declare Scope ladder_type_scope.
Declare Scope ladder_expr_scope.
Declare Custom Entry ladder_type.
Declare Custom Entry ladder_expr.
Notation "[< t >]" := t
(t custom ladder_type at level 99) : ladder_type_scope.
Notation "t" := t
(in custom ladder_type at level 0, t ident) : ladder_type_scope.
Notation "'∀' t" := (ty_univ t)
(t custom ladder_type at level 80, in custom ladder_type at level 80).
Notation "'<' σ τ '>'" := (ty_spec σ τ)
(in custom ladder_type at level 80, left associativity) : ladder_type_scope.
Notation "'[' τ ']'" := (ty_spec (ty_id "Seq") τ)
(in custom ladder_type at level 70) : ladder_type_scope.
Notation "'(' τ ')'" := τ
(in custom ladder_type at level 5) : ladder_type_scope.
Notation "σ '->' τ" := (ty_func σ τ)
(in custom ladder_type at level 75, right associativity) : ladder_type_scope.
Notation "σ '->morph' τ" := (ty_morph σ τ)
(in custom ladder_type at level 75, right associativity, τ at level 80) : ladder_type_scope.
Notation "σ '~' τ" := (ty_ladder σ τ)
(in custom ladder_type at level 20, right associativity) : ladder_type_scope.
Notation "'$' x" := (ty_id x%string)
(in custom ladder_type at level 10, x constr) : ladder_type_scope.
Notation "'%' x" := (ty_fvar x)
(in custom ladder_type at level 10, x constr) : ladder_type_scope.
Notation "[{ e }]" := e
(e custom ladder_expr at level 99) : ladder_expr_scope.
Notation "e" := e
(in custom ladder_expr at level 0, e ident) : ladder_expr_scope.
Notation "'$' x" := (ex_fvar x)
(in custom ladder_expr at level 10, x constr) : ladder_expr_scope.
Notation "'%' x" := (ex_bvar x)
(in custom ladder_expr at level 10, x constr) : ladder_expr_scope.
Notation "'Λ' e" := (ex_ty_abs e)
(in custom ladder_expr at level 10, e custom ladder_expr at level 80, right associativity) : ladder_expr_scope.
Notation "'λ' τ '↦' e" := (ex_abs τ e)
(in custom ladder_expr at level 70, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope.
Notation "'λ' τ '↦morph' e" := (ex_morph τ e)
(in custom ladder_expr at level 70, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope.
Notation "'let' e 'in' t" := (ex_let e t)
(in custom ladder_expr at level 60, e custom ladder_expr at level 80, t custom ladder_expr at level 80, right associativity) : ladder_expr_scope.
Notation "e 'as' τ" := (ex_ascend τ e)
(in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
Notation "e 'des' τ" := (ex_descend τ e)
(in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
Notation "e1 e2" := (ex_app e1 e2)
(in custom ladder_expr at level 90, e2 custom ladder_expr at next level) : ladder_expr_scope.
Notation "e '#' τ" := (ex_ty_app e τ)
(in custom ladder_expr at level 80, τ custom ladder_type at level 101, left associativity) : ladder_expr_scope.
Notation "'(' e ')'" := e
(in custom ladder_expr, e custom ladder_expr at next level, left associativity) : ladder_expr_scope.
(* get the list of all free variables in a type term *)
Fixpoint type_fv (τ : type_DeBruijn) {struct τ} : atoms :=
match τ with