max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-06 13:10:58 -07:00
parent 1be41f2adb
commit 75872189cc
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/PPRoundtrip.lean.expected.out
View file

@ -54,12 +54,11 @@ decide (1 < 2) ||
true
id (fun a => a) 0
typeAs Nat
(do
let x ← pure 1
(let x := 1;
do
discard (pure 2)
let y : Nat := 3
pure (x + y) :
Id Nat)
pure (x + y))
typeAs (Id Nat)
(pure 1 >>= pure)
(0 ≤ 1) = False