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

feat(library): remove occurrences of 'opaque' keyword

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-08 16:40:03 -07:00
parent cf7e60e5a6
commit 4f0f739ea6
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/logic.lean
View file

@ -415,7 +415,7 @@ inhabited.rec H2 H1
definition default (A : Type) [H : inhabited A] : A := definition default (A : Type) [H : inhabited A] : A :=
inhabited.rec (λa, a) H 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 inhabited.rec (λa, a) H
definition Prop.is_inhabited [instance] : inhabited Prop := definition Prop.is_inhabited [instance] : inhabited Prop :=

2
library/tools/fake_simplifier.lean
View file

@ -3,6 +3,6 @@ open tactic
namespace fake_simplifier namespace fake_simplifier
-- until we have the simplifier... -- until we have the simplifier...
opaque definition simp : tactic := apply sorry definition simp : tactic := apply sorry
end fake_simplifier end fake_simplifier