chore: fix tests
This commit is contained in:
Leonardo de Moura
parent
1512ccfdc8
commit
d0d3e24975
2 changed files with 35 additions and 25 deletions
|
|
@ -266,9 +266,11 @@ match x with
|
|||
(null (Term.id `x (null)))
|
||||
(null)
|
||||
"with"
|
||||
(null "|")
|
||||
(null
|
||||
(Term.matchAlt "|" (null (Term.app (Term.id `some (null)) (null (Term.id `x (null))))) "=>" (Term.id `true (null)))
|
||||
(Term.matchAlt "|" (null (Term.id `none (null))) "=>" (Term.id `false (null)))))
|
||||
(Term.matchAlt (null (Term.app (Term.id `some (null)) (null (Term.id `x (null))))) "=>" (Term.id `true (null)))
|
||||
"|"
|
||||
(Term.matchAlt (null (Term.id `none (null))) "=>" (Term.id `false (null)))))
|
||||
|
||||
match x with
|
||||
| some y => match y with
|
||||
|
|
@ -281,9 +283,9 @@ match x with
|
|||
(null (Term.id `x (null)))
|
||||
(null)
|
||||
"with"
|
||||
(null "|")
|
||||
(null
|
||||
(Term.matchAlt
|
||||
"|"
|
||||
(null (Term.app (Term.id `some (null)) (null (Term.id `y (null)))))
|
||||
"=>"
|
||||
(Term.match
|
||||
|
|
@ -291,17 +293,19 @@ match x with
|
|||
(null (Term.id `y (null)))
|
||||
(null)
|
||||
"with"
|
||||
(null "|")
|
||||
(null
|
||||
(Term.matchAlt
|
||||
"|"
|
||||
(null
|
||||
(Term.app
|
||||
(Term.id `some (null))
|
||||
(null (Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")"))))
|
||||
"=>"
|
||||
(Term.add (Term.id `a (null)) "+" (Term.id `b (null))))
|
||||
(Term.matchAlt "|" (null (Term.id `none (null))) "=>" (Term.num (numLit "1"))))))
|
||||
(Term.matchAlt "|" (null (Term.id `none (null))) "=>" (Term.num (numLit "0")))))
|
||||
"|"
|
||||
(Term.matchAlt (null (Term.id `none (null))) "=>" (Term.num (numLit "1"))))))
|
||||
"|"
|
||||
(Term.matchAlt (null (Term.id `none (null))) "=>" (Term.num (numLit "0")))))
|
||||
Type u
|
||||
(Term.sortApp (Term.type "Type") (Level.ident `u))
|
||||
Sort v
|
||||
|
|
@ -313,19 +317,19 @@ f Type 1
|
|||
let x := 0; x + 1
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letIdDecl `x (null) (null) ":=" (Term.num (numLit "0")))
|
||||
(Term.letDecl `x (null) (null) ":=" (Term.num (numLit "0")))
|
||||
";"
|
||||
(Term.add (Term.id `x (null)) "+" (Term.num (numLit "1"))))
|
||||
let x : Nat := 0; x + 1
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letIdDecl `x (null) (null (Term.typeSpec ":" (Term.id `Nat (null)))) ":=" (Term.num (numLit "0")))
|
||||
(Term.letDecl `x (null) (null (Term.typeSpec ":" (Term.id `Nat (null)))) ":=" (Term.num (numLit "0")))
|
||||
";"
|
||||
(Term.add (Term.id `x (null)) "+" (Term.num (numLit "1"))))
|
||||
let f (x : Nat) := x + 1; f 0
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letIdDecl
|
||||
(Term.letDecl
|
||||
`f
|
||||
(null (Term.explicitBinder "(" (null `x) (null ":" (Term.id `Nat (null))) (null) ")"))
|
||||
(null)
|
||||
|
|
@ -336,7 +340,7 @@ let f (x : Nat) := x + 1; f 0
|
|||
let f {α : Type} (a : α) : α := a; f 10
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letIdDecl
|
||||
(Term.letDecl
|
||||
`f
|
||||
(null
|
||||
(Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type")) "}")
|
||||
|
|
@ -349,7 +353,7 @@ let f {α : Type} (a : α) : α := a; f 10
|
|||
let f (x) := x + 1; f 10 + f 20
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letIdDecl
|
||||
(Term.letDecl
|
||||
`f
|
||||
(null (Term.explicitBinder "(" (null `x) (null) (null) ")"))
|
||||
(null)
|
||||
|
|
@ -363,9 +367,10 @@ let f (x) := x + 1; f 10 + f 20
|
|||
let (x, y) := f 10; x + y
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letPatDecl
|
||||
(Term.letDecl
|
||||
(Term.paren "(" (null (Term.id `x (null)) (null (Term.tupleTail "," (null (Term.id `y (null)))))) ")")
|
||||
(null)
|
||||
(null)
|
||||
":="
|
||||
(Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
|
||||
";"
|
||||
|
|
@ -373,13 +378,14 @@ let (x, y) := f 10; x + y
|
|||
let { fst := x, .. } := f 10; x + x
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letPatDecl
|
||||
(Term.letDecl
|
||||
(Term.structInst
|
||||
"{"
|
||||
(null)
|
||||
(null (Term.structInstField `fst ":=" (Term.id `x (null))) "," (Term.structInstSource ".." (null)))
|
||||
"}")
|
||||
(null)
|
||||
(null)
|
||||
":="
|
||||
(Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
|
||||
";"
|
||||
|
|
@ -387,15 +393,16 @@ let { fst := x, .. } := f 10; x + x
|
|||
let x.y := f 10; x
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letIdDecl `x.y (null) (null) ":=" (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
|
||||
(Term.letDecl `x.y (null) (null) ":=" (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
|
||||
";"
|
||||
(Term.id `x (null)))
|
||||
let x.1 := f 10; x
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letPatDecl
|
||||
(Term.letDecl
|
||||
(Term.proj (Term.id `x (null)) "." (fieldIdx "1"))
|
||||
(null)
|
||||
(null)
|
||||
":="
|
||||
(Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
|
||||
";"
|
||||
|
|
@ -403,9 +410,10 @@ let x.1 := f 10; x
|
|||
let x[i].y := f 10; x
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letPatDecl
|
||||
(Term.letDecl
|
||||
(Term.proj (Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]") "." `y)
|
||||
(null)
|
||||
(null)
|
||||
":="
|
||||
(Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
|
||||
";"
|
||||
|
|
@ -413,9 +421,10 @@ let x[i].y := f 10; x
|
|||
let x[i] := f 20; x
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letPatDecl
|
||||
(Term.letDecl
|
||||
(Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]")
|
||||
(null)
|
||||
(null)
|
||||
":="
|
||||
(Term.app (Term.id `f (null)) (null (Term.num (numLit "20")))))
|
||||
";"
|
||||
|
|
@ -448,7 +457,7 @@ do
|
|||
";"
|
||||
(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.doLet "let" (Term.letDecl `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)))))) ")")
|
||||
|
|
@ -458,9 +467,10 @@ do
|
|||
";"
|
||||
(Term.doLet
|
||||
"let"
|
||||
(Term.letPatDecl
|
||||
(Term.letDecl
|
||||
(Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")")
|
||||
(null)
|
||||
(null)
|
||||
":="
|
||||
(Term.paren "(" (null (Term.id `b (null)) (null (Term.tupleTail "," (null (Term.id `a (null)))))) ")")))
|
||||
";"
|
||||
|
|
@ -484,19 +494,19 @@ let f : Nat → Nat → Nat
|
|||
f 20
|
||||
(Term.let
|
||||
"let"
|
||||
(Term.letEqns
|
||||
(Term.letDecl
|
||||
`f
|
||||
(null)
|
||||
(null
|
||||
(Term.typeSpec ":" (Term.arrow (Term.id `Nat (null)) "→" (Term.arrow (Term.id `Nat (null)) "→" (Term.id `Nat (null))))))
|
||||
"|"
|
||||
(null
|
||||
(Term.matchAlt
|
||||
"|"
|
||||
(null (Term.num (numLit "0")) "," (Term.id `a (null)))
|
||||
"=>"
|
||||
(Term.add (Term.id `a (null)) "+" (Term.num (numLit "10"))))
|
||||
"|"
|
||||
(Term.matchAlt
|
||||
"|"
|
||||
(null (Term.add (Term.id `n (null)) "+" (Term.num (numLit "1"))) "," (Term.id `b (null)))
|
||||
"=>"
|
||||
(Term.mul (Term.id `n (null)) "*" (Term.id `b (null))))))
|
||||
|
|
@ -509,6 +519,6 @@ failed as expected, error: <input>:1:10 found '→' as expected, but brackets ar
|
|||
(x := 20)
|
||||
failed as expected, error: <input>:1:3 expected ':' or ')'
|
||||
let x 10; x
|
||||
failed as expected, error: <input>:1:8 expected ':='
|
||||
failed as expected, error: <input>:1:6 expected '|'
|
||||
let x := y
|
||||
failed as expected, error: <input>:1:10 expected ';'
|
||||
|
|
|
|||
|
|
@ -25,5 +25,5 @@
|
|||
"(Term.simpleBinder (null (Term.hole \"_\")))"
|
||||
"`a._@.UnhygienicMain._hyg.1"
|
||||
"(Term.id `a._@.UnhygienicMain._hyg.1 (null (Term.explicitUniv \".{\" (null (Level.num (numLit \"0\"))) \"}\")))"
|
||||
"#[(Term.matchAlt \"|\" (null (Term.id `a._@.UnhygienicMain._hyg.1 (null))) \"=>\" (Term.num (numLit \"1\"))), (Term.matchAlt \"|\" (null (Term.hole \"_\")) \"=>\" (Term.num (numLit \"2\")))]"
|
||||
"#[(Term.matchAlt \"|\" (null (Term.id `a._@.UnhygienicMain._hyg.1 (null))) \"=>\" (Term.num (numLit \"1\"))), (Term.matchAlt \"|\" (null (Term.hole \"_\")) \"=>\" (Term.num (numLit \"2\")))]"
|
||||
"#[]"
|
||||
StxQuot.lean:40:74: error: expected '⇒', '=>'
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue