diff options
Diffstat (limited to 'test-suite/output/Notations3.v')
| -rw-r--r-- | test-suite/output/Notations3.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 9f6302f6f2..b4ad4a7b3c 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -383,3 +383,11 @@ Check fun '(((x,y),true)|((x,y),false)) => x+y. Check myexists (((x,y),true)|((x,y),false)), x>y. Check exists '(((x,y),true)|((x,y),false)), x>y. Check ∀ '(((x,y),true)|((x,y),false)), x>y. + +(* Check Georges' printability of a "if is then else" notation *) + +Notation "'if' c 'is' p 'then' u 'else' v" := + (match c with p => u | _ => v end) + (at level 200, p pattern at level 100). +Check fun p => if p is S n then n else 0. +Check fun p => if p is Lt then 1 else 0. |