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

chore(tests): update test output

Browse source
This commit is contained in:
Gabriel Ebner 2017-09-06 14:27:39 +02:00
parent 5f8cf45073
commit 5adb3630b2
4 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/coe1.lean.expected.out
View file

@ -1,4 +1,4 @@
ite ↑tt "a" "b" : string
ite ↥tt "a" "b" : string
sine x : real
sine ↑n : real
sine ↑i : real

2
tests/lean/coe2.lean.expected.out
View file

@ -1,4 +1,4 @@
ite tt "a" "b" : string
ite ↥tt "a" "b" : string
sine x : real
sine n : real
sine i : real

2
tests/lean/no_coe.lean.expected.out
View file

@ -1,4 +1,4 @@
ite ↑tt 1 0 : ℕ
ite ↥tt 1 0 : ℕ
no_coe.lean:5:7: error: type mismatch at application
ite tt
term

2
tests/lean/print_meta.lean.expected.out
View file

@ -2,4 +2,4 @@ meta def tactic.intro : name → tactic expr :=
λ (n : name),
tactic.target >>=
λ (t : expr),
ite (↑(expr.is_pi t) ∨ ↑(expr.is_let t)) (tactic.intro_core n) (tactic.whnf_target >> tactic.intro_core n)
ite (↥(expr.is_pi t) ∨ ↥(expr.is_let t)) (tactic.intro_core n) (tactic.whnf_target >> tactic.intro_core n)