From 40ef589d8c19b776dd3907d51eeae1b5eae59e62 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 15 Aug 2015 09:48:05 -0700 Subject: [PATCH] fix(library/data/finset,library/data/list): fixes #799 Make sure standard library - theories folder can be compiled with --to_axiom --- library/data/finset/equiv.lean | 2 +- library/data/list/comb.lean | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/library/data/finset/equiv.lean b/library/data/finset/equiv.lean index 0b1b95066f..2de7a0bf6c 100644 --- a/library/data/finset/equiv.lean +++ b/library/data/finset/equiv.lean @@ -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 diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean index 229db0c034..030b4c937d 100644 --- a/library/data/list/comb.lean +++ b/library/data/list/comb.lean @@ -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