From 7b84df346c6a56b1b51cce73078411767122caa4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 18 Feb 2018 15:45:16 -0500 Subject: Add notations for type reification --- src/Experiments/SimplyTypedArithmetic.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/Experiments/SimplyTypedArithmetic.v') diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 44beaa3ee..c033b4c88 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -329,6 +329,9 @@ Module Compilers. constr:(type_primitive rt) end. + Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing). + Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing). + Module Export Notations. Export Coercions. Delimit Scope ctype_scope with ctype. -- cgit v1.2.3