From faf19678f399c920d28beac127e5c9df81341097 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 7 Dec 2023 15:22:45 -0800 Subject: [PATCH] Add `subst!` and `typeof!` to `Notations.v` --- src/Util/Notations.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 384dad1eed..0a780d26ee 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -205,3 +205,6 @@ Reserved Notation "##### x" (at level 9, x at level 9, format "##### x"). Reserved Notation "\ x .. y , t" (at level 200, x binder, y binder, right associativity, format "\ x .. y , '//' t"). (** If we use "( x |? y )", it conflicts with things like [destruct x as [?|?]; ...] *) Reserved Notation "( x | ? y )" (format "( x | ? y )"). + +Notation "'subst!' y 'for' x 'in' f" := (match y with x => f end) (at level 10, only parsing). +Notation "'typeof!' x" := (match _ as T with T => subst! x : T for _ in T end) (at level 10, only parsing).