From 4f0f739ea60ebf14d60e014cc25a0985564f522f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 May 2015 16:40:03 -0700 Subject: [PATCH] feat(library): remove occurrences of 'opaque' keyword --- library/init/logic.lean | 2 +- library/tools/fake_simplifier.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/logic.lean b/library/init/logic.lean index 23a777e70..b5728fefc 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -415,7 +415,7 @@ inhabited.rec H2 H1 definition default (A : Type) [H : inhabited A] : A := inhabited.rec (λa, a) H -opaque definition arbitrary (A : Type) [H : inhabited A] : A := +definition arbitrary [irreducible] (A : Type) [H : inhabited A] : A := inhabited.rec (λa, a) H definition Prop.is_inhabited [instance] : inhabited Prop := diff --git a/library/tools/fake_simplifier.lean b/library/tools/fake_simplifier.lean index 4f3bf0702..ff5bf6273 100644 --- a/library/tools/fake_simplifier.lean +++ b/library/tools/fake_simplifier.lean @@ -3,6 +3,6 @@ open tactic namespace fake_simplifier -- until we have the simplifier... -opaque definition simp : tactic := apply sorry +definition simp : tactic := apply sorry end fake_simplifier