michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean): test discrepancy on OSX

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-27 23:31:35 -08:00
parent dbdbd211e3
commit db45d02078
2 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tests/lean/simp32.lean
View file

@ -20,7 +20,6 @@ variable f {A : Type} : A → A
local m = simplifier_monitor(nil, nil, nil, local m = simplifier_monitor(nil, nil, nil,
function (s, e, i, k) function (s, e, i, k)
print("App simplification failure, argument #" .. i) print("App simplification failure, argument #" .. i)
print(e)
print("Kind: " .. k) print("Kind: " .. k)
print("-----------") print("-----------")
end, end,

1
tests/lean/simp32.lean.expected.out
View file

@ -10,7 +10,6 @@
λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val == (λ (n : ℕ) (v : vec (n + 0)), v) val λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val == (λ (n : ℕ) (v : vec (n + 0)), v) val
=====> =====>
App simplification failure, argument #2 App simplification failure, argument #2
(λ (n : ℕ) (v : vec (n + 0)), f v ; empty) 2::1 == (λ (n : ℕ) (v : vec (n + 0)), v) 2::1
Kind: 0 Kind: 0
----------- -----------
λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val == (λ (n : ℕ) (v : vec (n + 0)), v) val λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val == (λ (n : ℕ) (v : vec (n + 0)), v) val