From 5adb3630b23200f4612a6407e62ef1eb72b00a1a Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 6 Sep 2017 14:27:39 +0200 Subject: [PATCH] chore(tests): update test output --- tests/lean/coe1.lean.expected.out | 2 +- tests/lean/coe2.lean.expected.out | 2 +- tests/lean/no_coe.lean.expected.out | 2 +- tests/lean/print_meta.lean.expected.out | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/lean/coe1.lean.expected.out b/tests/lean/coe1.lean.expected.out index bc5249e4c7..c12964325d 100644 --- a/tests/lean/coe1.lean.expected.out +++ b/tests/lean/coe1.lean.expected.out @@ -1,4 +1,4 @@ -ite ↑tt "a" "b" : string +ite ↥tt "a" "b" : string sine x : real sine ↑n : real sine ↑i : real diff --git a/tests/lean/coe2.lean.expected.out b/tests/lean/coe2.lean.expected.out index af71e818b8..0d9f349b97 100644 --- a/tests/lean/coe2.lean.expected.out +++ b/tests/lean/coe2.lean.expected.out @@ -1,4 +1,4 @@ -ite tt "a" "b" : string +ite ↥tt "a" "b" : string sine x : real sine n : real sine i : real diff --git a/tests/lean/no_coe.lean.expected.out b/tests/lean/no_coe.lean.expected.out index bd6ffb145d..d6cc003bd8 100644 --- a/tests/lean/no_coe.lean.expected.out +++ b/tests/lean/no_coe.lean.expected.out @@ -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 diff --git a/tests/lean/print_meta.lean.expected.out b/tests/lean/print_meta.lean.expected.out index 54e150f8d0..bf12d5cba3 100644 --- a/tests/lean/print_meta.lean.expected.out +++ b/tests/lean/print_meta.lean.expected.out @@ -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)