From 2a451abe5221fd394ab78523fb0e143007ada863 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 2 Mar 2025 13:42:50 -0500 Subject: [PATCH] Add some reduction notations --- src/Util/Notations.v | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Util/Notations.v b/src/Util/Notations.v index b99ccf35f1..fd41c3e10f 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -207,3 +207,11 @@ Reserved Notation "\ x .. y , t" (at level 200, x binder, y binder, right associ Reserved Notation "( x | ? y )" (format "( x | ? y )"). Notation "'typeof!' x" := (match x with y => ltac:(let T := type of y in exact T) end) (at level 10, only parsing). + +Notation "'compute!' x" := (match x with y => ltac:(let z := (eval compute in y) in exact z) end) (at level 10, only parsing). +Notation "'cbv!' x" := (match x with y => ltac:(let z := (eval cbv in y) in exact z) end) (at level 10, only parsing). +Notation "'lazy!' x" := (match x with y => ltac:(let z := (eval lazy in y) in exact z) end) (at level 10, only parsing). +Notation "'cbn!' x" := (match x with y => ltac:(let z := (eval cbn in y) in exact z) end) (at level 10, only parsing). +Notation "'simpl!' x" := (match x with y => ltac:(let z := (eval simpl in y) in exact z) end) (at level 10, only parsing). +Notation "'native_compute!' x" := (match x with y => ltac:(let z := (eval native_compute in y) in exact z) end) (at level 10, only parsing). +Notation "'vm_compute!' x" := (match x with y => ltac:(let z := (eval vm_compute in y) in exact z) end) (at level 10, only parsing).