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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-20 22:26:07 -08:00
parent b279433236
commit 7e61315e6d
1 changed files with 34 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

70
tests/compiler/termparsertest1.lean.expected.out
View file

@ -437,48 +437,46 @@ do
pure (a + b)
(Term.do
"do"
(Term.doSeq
(null
(Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (null (Term.id `a (null)))))
";"
(Term.doId
`x
(null (Term.typeSpec ":" (Term.id `Nat (null))))
"←"
(Term.app (Term.id `f (null)) (null (Term.id `a (null)))))
";"
(Term.doExpr (Term.app (Term.id `g (null)) (null (Term.id `x (null)))))
";"
(Term.doLet "let" (Term.letIdDecl `y (null) (null) ":=" (Term.app (Term.id `g (null)) (null (Term.id `x (null))))))
";"
(Term.doPat
(null
(Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (null (Term.id `a (null)))))
";"
(Term.doId
`x
(null (Term.typeSpec ":" (Term.id `Nat (null))))
"←"
(Term.app (Term.id `f (null)) (null (Term.id `a (null)))))
";"
(Term.doExpr (Term.app (Term.id `g (null)) (null (Term.id `x (null)))))
";"
(Term.doLet "let" (Term.letIdDecl `y (null) (null) ":=" (Term.app (Term.id `g (null)) (null (Term.id `x (null))))))
";"
(Term.doPat
(Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")")
"<-"
(Term.app (Term.id `h (null)) (null (Term.id `x (null)) (Term.id `y (null))))
(null))
";"
(Term.doLet
"let"
(Term.letPatDecl
(Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")")
"<-"
(Term.app (Term.id `h (null)) (null (Term.id `x (null)) (Term.id `y (null))))
(null))
";"
(Term.doLet
"let"
(Term.letPatDecl
(Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")")
(null)
":="
(Term.paren "(" (null (Term.id `b (null)) (null (Term.tupleTail "," (null (Term.id `a (null)))))) ")")))
";"
(Term.doExpr
(Term.app
(Term.id `pure (null))
(null (Term.paren "(" (null (Term.add (Term.id `a (null)) "+" (Term.id `b (null))) (null)) ")")))))))
(null)
":="
(Term.paren "(" (null (Term.id `b (null)) (null (Term.tupleTail "," (null (Term.id `a (null)))))) ")")))
";"
(Term.doExpr
(Term.app
(Term.id `pure (null))
(null (Term.paren "(" (null (Term.add (Term.id `a (null)) "+" (Term.id `b (null))) (null)) ")"))))))
do { x ← f a; pure $ a + a }
(Term.do
"do"
(Term.bracketedDoSeq
"{"
(Term.doSeq
(null
(Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (null (Term.id `a (null)))))
";"
(Term.doExpr (Term.dollar (Term.id `pure (null)) "$" (Term.add (Term.id `a (null)) "+" (Term.id `a (null)))))))
(null
(Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (null (Term.id `a (null)))))
";"
(Term.doExpr (Term.dollar (Term.id `pure (null)) "$" (Term.add (Term.id `a (null)) "+" (Term.id `a (null))))))
"}"))
let f : Nat → Nat → Nat
| 0, a => a + 10