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

fix(frontends/lean): coercion affects other modules

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-10 20:14:19 -08:00
parent 64043094f4
commit 22b7a0615f
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/logic/wf.lean
View file

@ -16,10 +16,10 @@ end acc
inductive well_founded [class] {A : Type} (R : A → A → Prop) : Prop := inductive well_founded [class] {A : Type} (R : A → A → Prop) : Prop :=
intro : (∀ a, acc R a) → well_founded R intro : (∀ a, acc R a) → well_founded R
definition well_founded.apply [coercion] {A : Type} {R : A → A → Prop} (wf : well_founded R) : ∀a, acc R a :=
take a, well_founded.rec_on wf (λp, p) a
namespace well_founded namespace well_founded
definition apply [coercion] {A : Type} {R : A → A → Prop} (wf : well_founded R) : ∀a, acc R a :=
take a, well_founded.rec_on wf (λp, p) a
context context
parameters {A : Type} {R : A → A → Prop} parameters {A : Type} {R : A → A → Prop}
infix `≺`:50 := R infix `≺`:50 := R
@ -67,6 +67,8 @@ namespace well_founded
end well_founded end well_founded
open well_founded
-- Empty relation is well-founded -- Empty relation is well-founded
definition empty.wf {A : Type} : well_founded (λa b : A, false) := definition empty.wf {A : Type} : well_founded (λa b : A, false) :=
well_founded.intro (λ (a : A), well_founded.intro (λ (a : A),