https://github.com/EasyCrypt/easycrypt
Revision ee26cc55310c92dae5f6afeb38d2b2ea9413569e authored by Alley Stoughton on 15 May 2023, 19:51:42 UTC, committed by Pierre-Yves Strub on 16 May 2023, 07:04:10 UTC
require import AllCore List. type t = [ A of int | B of bool]. (* the following formulas now parse and pretty-print the same *) lemma foo1 (f : int -> bool) : f (match A 3 with | A a => a | B b => if b then 1 else 2 end). proof. abort. lemma foo2 : (match A 3 with | A a => fun _ => a | B b => fun _ => 2 end) 3 = 4. proof. abort. lemma foo3 (f : (int -> int) -> (int -> int)) : f (match A 3 with | A a => fun _ => a | B b => fun _ => 2 end) 3 = 4. proof. abort. lemma foo4 (f : int -> bool) : f (1 + match A 3 with | A a => a | B b => if b then 1 else 2 end). proof. abort. lemma foo5 (f : int -> bool) : f (match A 3 with | A a => a | B b => if b then 1 else 2 end + 1). proof. abort. lemma foo6 (f : int -> bool) : f (3 + match A 3 with | A a => a | B b => if b then 1 else 2 end + 1). proof. abort.
1 parent 94538c5
Tip revision: ee26cc55310c92dae5f6afeb38d2b2ea9413569e authored by Alley Stoughton on 15 May 2023, 19:51:42 UTC
Commit b2106aa suppressed additional parentheses around match ... end in all circumstances, even though on the left and right of applications the parser requires parentheses, the theory being this makes it easier for humans to scan. So this commit inserts parentheses around matches in applications, but not elsewhere (e.g., not in infix operators). See below for examples. [The pretty printer needs a major redesign, so this is another stopgap measure.]
Commit b2106aa suppressed additional parentheses around match ... end in all circumstances, even though on the left and right of applications the parser requires parentheses, the theory being this makes it easier for humans to scan. So this commit inserts parentheses around matches in applications, but not elsewhere (e.g., not in infix operators). See below for examples. [The pretty printer needs a major redesign, so this is another stopgap measure.]
Tip revision: ee26cc5
| File | Mode | Size |
|---|---|---|
| .github | ||
| config | ||
| examples | ||
| scripts | ||
| src | ||
| theories | ||
| .dir-locals.el | -rw-r--r-- | 285 bytes |
| .gitignore | -rw-r--r-- | 118 bytes |
| AUTHORS | -rw-r--r-- | 543 bytes |
| LICENSE | -rw-r--r-- | 1.2 KB |
| Makefile | -rw-r--r-- | 1.3 KB |
| README.md | -rw-r--r-- | 8.0 KB |
| default.nix | -rw-r--r-- | 921 bytes |
| dune | -rw-r--r-- | 221 bytes |
| dune-project | -rw-r--r-- | 450 bytes |
| easycrypt.opam | -rw-r--r-- | 1.2 KB |
| easycrypt.opam.template | -rw-r--r-- | 915 bytes |
| easycrypt.png | -rw-r--r-- | 182.6 KB |
| shell.nix | -rw-r--r-- | 741 bytes |
Computing file changes ...
