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

feat(library/init/quot): add rec_on for subsingleton types

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-01 11:57:39 -07:00
parent ce5e83eb3e
commit 0da4f191fc
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/quot.lean
View file

@ -63,6 +63,10 @@ namespace quot
protected definition rec_on [reducible] protected definition rec_on [reducible]
(q : quot s) (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b) : B q := (q : quot s) (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b) : B q :=
rec f H q rec f H q
protected definition rec_on_subsingleton [reducible]
[H : ∀ a, subsingleton (B ⟦a⟧)] (q : quot s) (f : Π a, B ⟦a⟧) : B q :=
rec f (λ a b h, !subsingleton.elim) q
end end
section section