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

feat(library/logic): import wf.lean in logic/default.lean

Browse source 
We will use well-founded recursion in the definitional package
This commit is contained in:
Leonardo de Moura 2014-11-06 15:03:13 -08:00
parent 194247f75b
commit 781f709bb4
3 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/logic/default.lean
View file

@ -2,7 +2,7 @@
--- Released under Apache 2.0 license as described in the file LICENSE. --- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad --- Author: Jeremy Avigad
import logic.connectives logic.eq logic.cast import logic.connectives logic.eq logic.cast logic.wf
import logic.quantifiers logic.if import logic.quantifiers logic.if
import logic.decidable logic.inhabited logic.nonempty import logic.decidable logic.inhabited logic.nonempty
import logic.instances import logic.instances

2
tests/lean/acc.lean
View file

@ -1,4 +1,4 @@
import logic import logic.prop
inductive acc (A : Type) (R : A → A → Prop) : A → Prop := inductive acc (A : Type) (R : A → A → Prop) : A → Prop :=
intro : ∀ (x : A), (∀ (y : A), R y x → acc A R y) → acc A R x intro : ∀ (x : A), (∀ (y : A), R y x → acc A R y) → acc A R x

2
tests/lean/acc_rec_bug.lean
View file

@ -1,4 +1,4 @@
import logic import logic.prop
inductive acc {A : Type} (R : A → A → Prop) : A → Prop := inductive acc {A : Type} (R : A → A → Prop) : A → Prop :=
intro : ∀x, (∀ y, R y x → acc R y) → acc R x intro : ∀x, (∀ y, R y x → acc R y) → acc R x