diff options
| -rw-r--r-- | src/Specific/IntegrationTestDisplayCommon.v | 6 | ||||
| -rw-r--r-- | src/Util/Notations.v | 2 |
2 files changed, 7 insertions, 1 deletions
diff --git a/src/Specific/IntegrationTestDisplayCommon.v b/src/Specific/IntegrationTestDisplayCommon.v index 123d0fb8a..f3acc3120 100644 --- a/src/Specific/IntegrationTestDisplayCommon.v +++ b/src/Specific/IntegrationTestDisplayCommon.v @@ -8,9 +8,11 @@ Require Export Coq.ZArith.ZArith. Require Export Crypto.Util.LetIn. Require Export Crypto.Util.FixedWordSizes. Require Export Crypto.Compilers.Z.CNotations. +Require Export Coq.Unicode.Utf8. (* for better line breaks at function display; must come last *) Global Arguments Pos.to_nat !_ / . Global Arguments InterpEta {_ _ _ _ _}. +Global Set Printing Width 2000000. Ltac display_helper f := let t := type of f in @@ -64,3 +66,7 @@ Tactic Notation "display" open_constr(f) := let ret := (eval cbv [interp_flat_type] in ret) in refine ret. Notation display f := (ltac:(let v := f in display v)) (only parsing). + +Notation "'Interp-η' f x" := (Eta.InterpEta f x) (format "'Interp-η' '//' f '//' x", at level 200, f at next level, x at next level). +Notation ReturnType := (interp_flat_type _). +Notation "'let' ( a , b ) := c 'in' d" := (let (a, b) := c in d) (at level 200, d at level 200, format "'let' ( a , b ) := c 'in' '//' d"). diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 327efb6df..962117925 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -78,7 +78,7 @@ Reserved Notation "'dlet' x := y 'in' f" (at level 200, f at level 200, format "'dlet' x := y 'in' '//' f"). Reserved Notation "'pflet' x , pf := y 'in' f" (at level 200, f at level 200, format "'pflet' x , pf := y 'in' '//' f"). -Reserved Notation "'λ' x .. y , t" (at level 200, x binder, y binder, right associativity). +Reserved Notation "'λ' x .. y , t" (at level 200, x binder, y binder, right associativity, format "'λ' x .. y , '//' t"). Reserved Notation "'λn' x .. y , t" (at level 200, right associativity). Reserved Notation "x ::> ( max_bitwidth = v )" (at level 70, no associativity, format "x ::> ( max_bitwidth = v )"). |