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

fix(library/data/finset,library/data/list): fixes #799

Browse source 
Make sure standard library - theories folder can be compiled with --to_axiom
This commit is contained in:
Leonardo de Moura 2015-08-15 09:48:05 -07:00
parent c83d592c17
commit 40ef589d8c
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/finset/equiv.lean
View file

@ -280,7 +280,7 @@ nat.strong_induction_on s
open equiv
lemma finset_nat_equiv_nat : finset nat ≃ nat :=
definition finset_nat_equiv_nat : finset nat ≃ nat :=
mk to_nat of_nat of_nat_to_nat to_nat_of_nat
end finset

10
library/data/list/comb.lean
View file

@ -467,11 +467,11 @@ end dmap
section
open equiv
lemma list_equiv_of_equiv {A B : Type} : A ≃ B → list A ≃ list B
definition list_equiv_of_equiv {A B : Type} : A ≃ B → list A ≃ list B
| (mk f g l r) :=
mk (map f) (map g)
begin intros, rewrite [map_map, id_of_left_inverse l, map_id] end
begin intros, rewrite [map_map, id_of_righ_inverse r, map_id] end
begin intros, rewrite [map_map, id_of_left_inverse l, map_id], try reflexivity end
begin intros, rewrite [map_map, id_of_righ_inverse r, map_id], try reflexivity end
private definition to_nat : list nat → nat
| [] := 0
@ -507,10 +507,10 @@ private lemma of_nat_to_nat : ∀ (l : list nat), of_nat (to_nat l) = l
| [] := rfl
| (x::xs) := begin unfold to_nat, rewrite of_nat_succ, rewrite *unpair_mkpair, esimp, congruence, apply of_nat_to_nat end
lemma list_nat_equiv_nat : list nat ≃ nat :=
definition list_nat_equiv_nat : list nat ≃ nat :=
mk to_nat of_nat of_nat_to_nat to_nat_of_nat
lemma list_equiv_self_of_equiv_nat {A : Type} : A ≃ nat → list A ≃ A :=
definition list_equiv_self_of_equiv_nat {A : Type} : A ≃ nat → list A ≃ A :=
suppose A ≃ nat, calc
list A ≃ list nat : list_equiv_of_equiv this
... ≃ nat : list_nat_equiv_nat