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

terms notation: add ident rule to allow variables in notation instance

Browse source
This commit is contained in:
Michael Sippel 2024-09-17 03:14:49 +02:00
parent f53f226f55
commit 127debf945
Signed by: senvas
GPG key ID: F96CF119C34B64A6
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
coq/terms.v
View file

@ -65,6 +65,8 @@ Declare Custom Entry ladder_expr.
Notation "[< t >]" := t
(t custom ladder_type at level 80) : ladder_type_scope.
Notation "t" := t
(in custom ladder_type at level 0, t ident) : ladder_type_scope.
Notation "'∀' x ',' t" := (type_univ x t)
(t custom ladder_type at level 80, in custom ladder_type at level 80, x constr).
Notation "'<' σ τ '>'" := (type_spec σ τ)
@ -84,6 +86,8 @@ Notation "'%' x '%'" := (type_var x%string)
Notation "[{ e }]" := e
(e custom ladder_expr at level 80) : ladder_expr_scope.
Notation "e" := e
(in custom ladder_expr at level 0, e ident) : ladder_expr_scope.
Notation "'%' x '%'" := (expr_var x%string)
(in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
Notation "'Λ' t '↦' e" := (expr_ty_abs t e)