From f3f1ec268b333d602defdb6f721c4e196199dde8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Dec 2016 18:22:37 -0800 Subject: [PATCH] chore(library/init/meta/tactic): make all arguments in id_locked explicit. --- library/init/meta/tactic.lean | 6 +++--- tests/lean/anc1.lean.expected.out | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 94adcc62e9..2c29168bd9 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -766,9 +766,9 @@ open tactic run_command do l ← return $ level.param `l, Ty ← return $ expr.sort l, - type ← to_expr `(Π {α : %%Ty}, α → α), - val ← to_expr `(λ {α : %%Ty} (a : α), a), + type ← to_expr `(Π (α : %%Ty), α → α), + val ← to_expr `(λ (α : %%Ty) (a : α), a), add_decl (declaration.defn `id_locked [`l] type val reducibility_hints.opaque tt) -lemma id_locked_eq {α : Type u} (a : α) : id_locked a = a := +lemma id_locked_eq {α : Type u} (a : α) : id_locked α a = a := rfl diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out index 8a83dd85a2..5996d30e91 100644 --- a/tests/lean/anc1.lean.expected.out +++ b/tests/lean/anc1.lean.expected.out @@ -2,7 +2,7 @@ and.intro trivial trivial : true ∧ true sigma.mk 1 sorry : Σ (x : ℕ), x > 0 show true, from true.intro : true -Exists.intro 1 (id_locked (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0 +Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from and.intro Hb Ha : ∀ (A B C : Prop), A → B → C → B ∧ A λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C),