From 127debf94525a3ca30013266e81081f38c8e3548 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Tue, 17 Sep 2024 03:14:49 +0200 Subject: [PATCH] terms notation: add ident rule to allow variables in notation instance --- coq/terms.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/coq/terms.v b/coq/terms.v index 00c075d..2ae8d33 100644 --- a/coq/terms.v +++ b/coq/terms.v @@ -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)