From 4b1b3e277f50e351da5b0a915fe40cb6e949ca54 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Jul 2015 16:37:06 -0700 Subject: [PATCH] feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]' see issue #693 --- .../category/constructions/comma.hlean | 6 +- hott/algebra/category/iso.hlean | 22 +++--- hott/arity.hlean | 4 +- hott/hit/circle.hlean | 16 ++-- hott/hit/coeq.hlean | 8 +- hott/hit/colimit.hlean | 16 ++-- hott/hit/cylinder.hlean | 8 +- hott/hit/pushout.hlean | 8 +- hott/hit/quotient.hlean | 8 +- hott/hit/red_susp.hlean | 8 +- hott/hit/refl_quotient.hlean | 8 +- hott/hit/set_quotient.hlean | 4 +- hott/hit/susp.hlean | 8 +- hott/hit/torus.hlean | 8 +- hott/hit/trunc.hlean | 6 +- hott/hit/two_quotient.hlean | 28 +++---- hott/init/datatypes.hlean | 8 +- hott/init/equiv.hlean | 8 +- hott/init/function.hlean | 24 +++--- hott/init/hit.hlean | 4 +- hott/init/logic.hlean | 6 +- hott/init/nat.hlean | 10 +-- hott/init/path.hlean | 62 +++++++-------- hott/init/pathover.hlean | 26 +++---- hott/init/trunc.hlean | 2 +- hott/types/W.hlean | 4 +- hott/types/cubical/square.hlean | 48 ++++++------ hott/types/eq.hlean | 2 +- hott/types/int/basic.hlean | 2 +- hott/types/pointed.hlean | 8 +- hott/types/sigma.hlean | 2 +- library/data/int/basic.lean | 2 +- library/data/stream.lean | 2 +- library/init/datatypes.lean | 4 +- library/init/function.lean | 22 +++--- library/init/nat.lean | 2 +- library/init/quot.lean | 18 ++--- src/emacs/lean-syntax.el | 4 +- src/frontends/lean/builtin_cmds.cpp | 13 +++- src/frontends/lean/decl_attributes.cpp | 30 +++---- src/frontends/lean/decl_attributes.h | 4 +- src/frontends/lean/structure_cmd.cpp | 4 +- src/frontends/lean/token_table.cpp | 4 +- src/frontends/lean/tokens.cpp | 24 ++++-- src/frontends/lean/tokens.h | 6 +- src/frontends/lean/tokens.txt | 6 +- src/library/definitional/brec_on.cpp | 4 +- src/library/definitional/cases_on.cpp | 2 +- src/library/definitional/projection.cpp | 2 +- src/library/definitional/rec_on.cpp | 2 +- src/library/normalize.cpp | 78 +++++++++---------- src/library/normalize.h | 20 ++--- tests/lean/640.hlean | 2 +- tests/lean/run/all_goals.lean | 4 +- tests/lean/run/all_goals2.lean | 4 +- tests/lean/run/rewriter14.lean | 4 +- tests/lean/unfoldf.lean | 4 +- 57 files changed, 336 insertions(+), 317 deletions(-) diff --git a/hott/algebra/category/constructions/comma.hlean b/hott/algebra/category/constructions/comma.hlean index caf1df24b..2d3dd637c 100644 --- a/hott/algebra/category/constructions/comma.hlean +++ b/hott/algebra/category/constructions/comma.hlean @@ -17,9 +17,9 @@ namespace category (a : A) (b : B) (f : S a ⟶ T b) - abbreviation ob1 [unfold-c 6] := @comma_object.a - abbreviation ob2 [unfold-c 6] := @comma_object.b - abbreviation mor [unfold-c 6] := @comma_object.f + abbreviation ob1 [unfold 6] := @comma_object.a + abbreviation ob2 [unfold 6] := @comma_object.b + abbreviation mor [unfold 6] := @comma_object.f variables {A B C : Precategory} (S : A ⇒ C) (T : B ⇒ C) diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index 8bc5b0dcd..c14026a8f 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -24,13 +24,13 @@ namespace iso attribute is_iso [multiple-instances] open split_mono split_epi is_iso - abbreviation retraction_of [unfold-c 6] := @split_mono.retraction_of - abbreviation retraction_comp [unfold-c 6] := @split_mono.retraction_comp - abbreviation section_of [unfold-c 6] := @split_epi.section_of - abbreviation comp_section [unfold-c 6] := @split_epi.comp_section - abbreviation inverse [unfold-c 6] := @is_iso.inverse - abbreviation left_inverse [unfold-c 6] := @is_iso.left_inverse - abbreviation right_inverse [unfold-c 6] := @is_iso.right_inverse + abbreviation retraction_of [unfold 6] := @split_mono.retraction_of + abbreviation retraction_comp [unfold 6] := @split_mono.retraction_comp + abbreviation section_of [unfold 6] := @split_epi.section_of + abbreviation comp_section [unfold 6] := @split_epi.comp_section + abbreviation inverse [unfold 6] := @is_iso.inverse + abbreviation left_inverse [unfold 6] := @is_iso.left_inverse + abbreviation right_inverse [unfold 6] := @is_iso.right_inverse postfix `⁻¹` := inverse --a second notation for the inverse, which is not overloaded postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse -- input using \-1h @@ -145,7 +145,7 @@ namespace iso (H1 : g ∘ f = id) (H2 : f ∘ g = id) := @mk _ _ _ _ f (is_iso.mk H1 H2) - definition to_inv [unfold-c 5] (f : a ≅ b) : b ⟶ a := + definition to_inv [unfold 5] (f : a ≅ b) : b ⟶ a := (to_hom f)⁻¹ protected definition refl [constructor] (a : ob) : a ≅ a := @@ -182,13 +182,13 @@ namespace iso apply equiv.to_is_equiv (!iso.sigma_char), end - definition iso_of_eq [unfold-c 5] (p : a = b) : a ≅ b := + definition iso_of_eq [unfold 5] (p : a = b) : a ≅ b := eq.rec_on p (iso.refl a) - definition hom_of_eq [reducible] [unfold-c 5] (p : a = b) : a ⟶ b := + definition hom_of_eq [reducible] [unfold 5] (p : a = b) : a ⟶ b := iso.to_hom (iso_of_eq p) - definition inv_of_eq [reducible] [unfold-c 5] (p : a = b) : b ⟶ a := + definition inv_of_eq [reducible] [unfold 5] (p : a = b) : b ⟶ a := iso.to_inv (iso_of_eq p) definition iso_of_eq_inv (p : a = b) : iso_of_eq p⁻¹ = iso.symm (iso_of_eq p) := diff --git a/hott/arity.hlean b/hott/arity.hlean index 8d19e009a..f4be844c9 100644 --- a/hott/arity.hlean +++ b/hott/arity.hlean @@ -121,10 +121,10 @@ namespace eq -- : f a b c d e ff g h = f a' b' c' d' e' f' g' h' := -- by cases Ha; cases Hb; cases Hc; cases Hd; cases He; cases Hf; cases Hg; cases Hh; reflexivity - definition apd100 [unfold-c 6] {f g : Πa b, C a b} (p : f = g) : f ~2 g := + definition apd100 [unfold 6] {f g : Πa b, C a b} (p : f = g) : f ~2 g := λa b, apd10 (apd10 p a) b - definition apd1000 [unfold-c 7] {f g : Πa b c, D a b c} (p : f = g) : f ~3 g := + definition apd1000 [unfold 7] {f g : Πa b c, D a b c} (p : f = g) : f ~3 g := λa b c, apd100 (apd10 p a) b c /- some properties of these variants of ap -/ diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean index c38898a34..d7a17712c 100644 --- a/hott/hit/circle.hlean +++ b/hott/hit/circle.hlean @@ -148,14 +148,14 @@ namespace circle end circle attribute circle.base1 circle.base2 circle.base [constructor] -attribute circle.rec2 circle.elim2 [unfold-c 6] [recursor 6] -attribute circle.elim2_type [unfold-c 5] -attribute circle.rec2_on circle.elim2_on [unfold-c 2] -attribute circle.elim2_type [unfold-c 1] -attribute circle.elim circle.rec [unfold-c 4] [recursor 4] -attribute circle.elim_type [unfold-c 3] -attribute circle.rec_on circle.elim_on [unfold-c 2] -attribute circle.elim_type_on [unfold-c 1] +attribute circle.rec2 circle.elim2 [unfold 6] [recursor 6] +attribute circle.elim2_type [unfold 5] +attribute circle.rec2_on circle.elim2_on [unfold 2] +attribute circle.elim2_type [unfold 1] +attribute circle.elim circle.rec [unfold 4] [recursor 4] +attribute circle.elim_type [unfold 3] +attribute circle.rec_on circle.elim_on [unfold 2] +attribute circle.elim_type_on [unfold 1] namespace circle definition pointed_circle [instance] [constructor] : pointed circle := diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index f485c9e8e..7cc5975fb 100644 --- a/hott/hit/coeq.hlean +++ b/hott/hit/coeq.hlean @@ -79,7 +79,7 @@ end end coeq attribute coeq.coeq_i [constructor] -attribute coeq.rec coeq.elim [unfold-c 8] [recursor 8] -attribute coeq.elim_type [unfold-c 7] -attribute coeq.rec_on coeq.elim_on [unfold-c 6] -attribute coeq.elim_type_on [unfold-c 5] +attribute coeq.rec coeq.elim [unfold 8] [recursor 8] +attribute coeq.elim_type [unfold 7] +attribute coeq.rec_on coeq.elim_on [unfold 6] +attribute coeq.elim_type_on [unfold 5] diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index 6df634042..220c40585 100644 --- a/hott/hit/colimit.hlean +++ b/hott/hit/colimit.hlean @@ -171,11 +171,11 @@ end end seq_colim attribute colimit.incl seq_colim.inclusion [constructor] -attribute colimit.rec colimit.elim [unfold-c 10] [recursor 10] -attribute colimit.elim_type [unfold-c 9] -attribute colimit.rec_on colimit.elim_on [unfold-c 8] -attribute colimit.elim_type_on [unfold-c 7] -attribute seq_colim.rec seq_colim.elim [unfold-c 6] [recursor 6] -attribute seq_colim.elim_type [unfold-c 5] -attribute seq_colim.rec_on seq_colim.elim_on [unfold-c 4] -attribute seq_colim.elim_type_on [unfold-c 3] +attribute colimit.rec colimit.elim [unfold 10] [recursor 10] +attribute colimit.elim_type [unfold 9] +attribute colimit.rec_on colimit.elim_on [unfold 8] +attribute colimit.elim_type_on [unfold 7] +attribute seq_colim.rec seq_colim.elim [unfold 6] [recursor 6] +attribute seq_colim.elim_type [unfold 5] +attribute seq_colim.rec_on seq_colim.elim_on [unfold 4] +attribute seq_colim.elim_type_on [unfold 3] diff --git a/hott/hit/cylinder.hlean b/hott/hit/cylinder.hlean index 1bc3e6850..917e8be63 100644 --- a/hott/hit/cylinder.hlean +++ b/hott/hit/cylinder.hlean @@ -89,7 +89,7 @@ end end cylinder attribute cylinder.base cylinder.top [constructor] -attribute cylinder.rec cylinder.elim [unfold-c 8] [recursor 8] -attribute cylinder.elim_type [unfold-c 7] -attribute cylinder.rec_on cylinder.elim_on [unfold-c 5] -attribute cylinder.elim_type_on [unfold-c 4] +attribute cylinder.rec cylinder.elim [unfold 8] [recursor 8] +attribute cylinder.elim_type [unfold 7] +attribute cylinder.rec_on cylinder.elim_on [unfold 5] +attribute cylinder.elim_type_on [unfold 4] diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index e93f4dbf1..ce380b9f3 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -86,7 +86,7 @@ end end pushout attribute pushout.inl pushout.inr [constructor] -attribute pushout.rec pushout.elim [unfold-c 10] [recursor 10] -attribute pushout.elim_type [unfold-c 9] -attribute pushout.rec_on pushout.elim_on [unfold-c 7] -attribute pushout.elim_type_on [unfold-c 6] +attribute pushout.rec pushout.elim [unfold 10] [recursor 10] +attribute pushout.elim_type [unfold 9] +attribute pushout.rec_on pushout.elim_on [unfold 7] +attribute pushout.elim_type_on [unfold 6] diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index 917b11d38..725b2670a 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -55,7 +55,7 @@ namespace quotient end quotient attribute quotient.rec [recursor] -attribute quotient.elim [unfold-c 6] [recursor 6] -attribute quotient.elim_type [unfold-c 5] -attribute quotient.elim_on [unfold-c 4] -attribute quotient.elim_type_on [unfold-c 3] +attribute quotient.elim [unfold 6] [recursor 6] +attribute quotient.elim_type [unfold 5] +attribute quotient.elim_on [unfold 4] +attribute quotient.elim_type_on [unfold 3] diff --git a/hott/hit/red_susp.hlean b/hott/hit/red_susp.hlean index c8cc7238f..cebb452d5 100644 --- a/hott/hit/red_susp.hlean +++ b/hott/hit/red_susp.hlean @@ -81,7 +81,7 @@ end end red_susp attribute red_susp.base [constructor] -attribute /-red_susp.rec-/ red_susp.elim [unfold-c 6] [recursor 6] ---attribute red_susp.elim_type [unfold-c 9] -attribute /-red_susp.rec_on-/ red_susp.elim_on [unfold-c 3] ---attribute red_susp.elim_type_on [unfold-c 6] +attribute /-red_susp.rec-/ red_susp.elim [unfold 6] [recursor 6] +--attribute red_susp.elim_type [unfold 9] +attribute /-red_susp.rec_on-/ red_susp.elim_on [unfold 3] +--attribute red_susp.elim_type_on [unfold 6] diff --git a/hott/hit/refl_quotient.hlean b/hott/hit/refl_quotient.hlean index 6ba1ed1df..374beaf89 100644 --- a/hott/hit/refl_quotient.hlean +++ b/hott/hit/refl_quotient.hlean @@ -84,7 +84,7 @@ end end refl_quotient attribute refl_quotient.rclass_of [constructor] -attribute /-refl_quotient.rec-/ refl_quotient.elim [unfold-c 8] [recursor 8] ---attribute refl_quotient.elim_type [unfold-c 9] -attribute /-refl_quotient.rec_on-/ refl_quotient.elim_on [unfold-c 5] ---attribute refl_quotient.elim_type_on [unfold-c 6] +attribute /-refl_quotient.rec-/ refl_quotient.elim [unfold 8] [recursor 8] +--attribute refl_quotient.elim_type [unfold 9] +attribute /-refl_quotient.rec_on-/ refl_quotient.elim_on [unfold 5] +--attribute refl_quotient.elim_type_on [unfold 6] diff --git a/hott/hit/set_quotient.hlean b/hott/hit/set_quotient.hlean index f12a16b35..bc1242d0f 100644 --- a/hott/hit/set_quotient.hlean +++ b/hott/hit/set_quotient.hlean @@ -71,5 +71,5 @@ end end set_quotient attribute set_quotient.class_of [constructor] -attribute set_quotient.rec set_quotient.elim [unfold-c 7] [recursor 7] -attribute set_quotient.rec_on set_quotient.elim_on [unfold-c 4] +attribute set_quotient.rec set_quotient.elim [unfold 7] [recursor 7] +attribute set_quotient.rec_on set_quotient.elim_on [unfold 4] diff --git a/hott/hit/susp.hlean b/hott/hit/susp.hlean index 1753b1a7a..3526fc001 100644 --- a/hott/hit/susp.hlean +++ b/hott/hit/susp.hlean @@ -72,10 +72,10 @@ namespace susp end susp attribute susp.north susp.south [constructor] -attribute susp.rec susp.elim [unfold-c 6] [recursor 6] -attribute susp.elim_type [unfold-c 5] -attribute susp.rec_on susp.elim_on [unfold-c 3] -attribute susp.elim_type_on [unfold-c 2] +attribute susp.rec susp.elim [unfold 6] [recursor 6] +attribute susp.elim_type [unfold 5] +attribute susp.rec_on susp.elim_on [unfold 3] +attribute susp.elim_type_on [unfold 2] namespace susp open pointed diff --git a/hott/hit/torus.hlean b/hott/hit/torus.hlean index ba7932e99..889ef24da 100644 --- a/hott/hit/torus.hlean +++ b/hott/hit/torus.hlean @@ -87,7 +87,7 @@ namespace torus end torus attribute torus.base [constructor] -attribute /-torus.rec-/ torus.elim [unfold-c 6] [recursor 6] ---attribute torus.elim_type [unfold-c 9] -attribute /-torus.rec_on-/ torus.elim_on [unfold-c 2] ---attribute torus.elim_type_on [unfold-c 6] +attribute /-torus.rec-/ torus.elim [unfold 6] [recursor 6] +--attribute torus.elim_type [unfold 9] +attribute /-torus.rec_on-/ torus.elim_on [unfold 2] +--attribute torus.elim_type_on [unfold 6] diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean index 4318ccf07..c003079dc 100644 --- a/hott/hit/trunc.hlean +++ b/hott/hit/trunc.hlean @@ -51,7 +51,7 @@ namespace trunc tr⁻¹ /- Functoriality -/ - definition trunc_functor [unfold-c 5] (f : X → Y) : trunc n X → trunc n Y := + definition trunc_functor [unfold 5] (f : X → Y) : trunc n X → trunc n Y := λxx, trunc.rec_on xx (λx, tr (f x)) definition trunc_functor_compose (f : X → Y) (g : Y → Z) @@ -130,6 +130,6 @@ namespace trunc end trunc -attribute trunc.elim_on [unfold-c 4] +attribute trunc.elim_on [unfold 4] attribute trunc.rec [recursor] -attribute trunc.elim [recursor 6] [unfold-c 6] +attribute trunc.elim [recursor 6] [unfold 6] diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index 3452230bf..493abf74e 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -34,10 +34,10 @@ namespace simple_two_quotient class_of pre_simple_two_quotient_rel (inr ⟨a, r, q⟩) protected definition e (s : R a a') : j a = j a' := eq_of_rel _ (pre_Rmk s) protected definition et (t : T a a') : j a = j a' := e_closure.elim e t - protected definition f [unfold-c 7] (q : Q r) : S¹ → C := + protected definition f [unfold 7] (q : Q r) : S¹ → C := circle.elim (j a) (et r) - protected definition pre_rec [unfold-c 8] {P : C → Type} + protected definition pre_rec [unfold 8] {P : C → Type} (Pj : Πa, P (j a)) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), P (pre_aux q)) (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a =[e s] Pj a') (x : C) : P x := begin @@ -48,7 +48,7 @@ namespace simple_two_quotient { induction H, esimp, apply Pe}, end - protected definition pre_elim [unfold-c 8] {P : Type} (Pj : A → P) + protected definition pre_elim [unfold 8] {P : Type} (Pj : A → P) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P) (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a = Pj a') (x : C) : P := pre_rec Pj Pa (λa a' s, pathover_of_eq (Pe s)) x @@ -124,7 +124,7 @@ namespace simple_two_quotient !ap_constant⁻¹ end } end end}, end - local attribute elim [unfold-c 8] + local attribute elim [unfold 8] protected definition elim_on {P : Type} (x : D) (P0 : A → P) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') @@ -237,10 +237,10 @@ end end simple_two_quotient --attribute simple_two_quotient.j [constructor] --TODO -attribute /-simple_two_quotient.rec-/ simple_two_quotient.elim [unfold-c 8] [recursor 8] ---attribute simple_two_quotient.elim_type [unfold-c 9] -attribute /-simple_two_quotient.rec_on-/ simple_two_quotient.elim_on [unfold-c 5] ---attribute simple_two_quotient.elim_type_on [unfold-c 6] +attribute /-simple_two_quotient.rec-/ simple_two_quotient.elim [unfold 8] [recursor 8] +--attribute simple_two_quotient.elim_type [unfold 9] +attribute /-simple_two_quotient.rec_on-/ simple_two_quotient.elim_on [unfold 5] +--attribute simple_two_quotient.elim_type_on [unfold 6] namespace two_quotient open e_closure simple_two_quotient @@ -272,11 +272,11 @@ namespace two_quotient induction x, { exact P0 a}, { exact P1 s}, - { exact abstract [unfold-c 10] begin induction q with a a' t t' q, + { exact abstract [unfold 10] begin induction q with a a' t t' q, rewrite [↑e_closure.elim,↓e_closure.elim P1 t,↓e_closure.elim P1 t'], apply con_inv_eq_idp, exact P2 q end end}, end - local attribute elim [unfold-c 8] + local attribute elim [unfold 8] protected definition elim_on {P : Type} (x : two_quotient) (P0 : A → P) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') @@ -314,7 +314,7 @@ end end two_quotient --attribute two_quotient.j [constructor] --TODO -attribute /-two_quotient.rec-/ two_quotient.elim [unfold-c 8] [recursor 8] ---attribute two_quotient.elim_type [unfold-c 9] -attribute /-two_quotient.rec_on-/ two_quotient.elim_on [unfold-c 5] ---attribute two_quotient.elim_type_on [unfold-c 6] +attribute /-two_quotient.rec-/ two_quotient.elim [unfold 8] [recursor 8] +--attribute two_quotient.elim_type [unfold 9] +attribute /-two_quotient.rec_on-/ two_quotient.elim_on [unfold 5] +--attribute two_quotient.elim_type_on [unfold 6] diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean index 8b8ea04bf..89ee1fa4f 100644 --- a/hott/init/datatypes.hlean +++ b/hott/init/datatypes.hlean @@ -31,10 +31,10 @@ up :: (down : A) inductive prod (A B : Type) := mk : A → B → prod A B -definition prod.pr1 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : A := +definition prod.pr1 [reducible] [unfold 3] {A B : Type} (p : prod A B) : A := prod.rec (λ a b, a) p -definition prod.pr2 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : B := +definition prod.pr2 [reducible] [unfold 3] {A B : Type} (p : prod A B) : B := prod.rec (λ a b, b) p definition prod.destruct [reducible] := @prod.cases_on @@ -52,10 +52,10 @@ sum.inr b inductive sigma {A : Type} (B : A → Type) := mk : Π (a : A), B a → sigma B -definition sigma.pr1 [reducible] [unfold-c 3] {A : Type} {B : A → Type} (p : sigma B) : A := +definition sigma.pr1 [reducible] [unfold 3] {A : Type} {B : A → Type} (p : sigma B) : A := sigma.rec (λ a b, a) p -definition sigma.pr2 [reducible] [unfold-c 3] {A : Type} {B : A → Type} (p : sigma B) : B (sigma.pr1 p) := +definition sigma.pr2 [reducible] [unfold 3] {A : Type} {B : A → Type} (p : sigma B) : B (sigma.pr1 p) := sigma.rec (λ a b, b) p -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26. diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index dee5d611c..4cb2162f6 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -232,14 +232,14 @@ namespace equiv (right_inv : f ∘ g ~ id) (left_inv : g ∘ f ~ id) : A ≃ B := equiv.mk f (adjointify f g right_inv left_inv) - definition to_inv [reducible] [unfold-c 3] (f : A ≃ B) : B → A := f⁻¹ - definition to_right_inv [reducible] [unfold-c 3] (f : A ≃ B) : f ∘ f⁻¹ ~ id := right_inv f - definition to_left_inv [reducible] [unfold-c 3] (f : A ≃ B) : f⁻¹ ∘ f ~ id := left_inv f + definition to_inv [reducible] [unfold 3] (f : A ≃ B) : B → A := f⁻¹ + definition to_right_inv [reducible] [unfold 3] (f : A ≃ B) : f ∘ f⁻¹ ~ id := right_inv f + definition to_left_inv [reducible] [unfold 3] (f : A ≃ B) : f⁻¹ ∘ f ~ id := left_inv f protected definition refl [refl] [constructor] : A ≃ A := equiv.mk id !is_equiv_id - protected definition symm [symm] [unfold-c 3] (f : A ≃ B) : B ≃ A := + protected definition symm [symm] [unfold 3] (f : A ≃ B) : B ≃ A := equiv.mk f⁻¹ !is_equiv_inv protected definition trans [trans] (f : A ≃ B) (g: B ≃ C) : A ≃ C := diff --git a/hott/init/function.hlean b/hott/init/function.hlean index 6efc39338..1e9b754a1 100644 --- a/hott/init/function.hlean +++ b/hott/init/function.hlean @@ -15,42 +15,42 @@ namespace function variables {A B C D E : Type} -definition compose [reducible] [unfold-f] (f : B → C) (g : A → B) : A → C := +definition compose [reducible] [unfold-full] (f : B → C) (g : A → B) : A → C := λx, f (g x) -definition compose_right [reducible] [unfold-f] (f : B → B → B) (g : A → B) : B → A → B := +definition compose_right [reducible] [unfold-full] (f : B → B → B) (g : A → B) : B → A → B := λ b a, f b (g a) -definition compose_left [reducible] [unfold-f] (f : B → B → B) (g : A → B) : A → B → B := +definition compose_left [reducible] [unfold-full] (f : B → B → B) (g : A → B) : A → B → B := λ a b, f (g a) b -definition id [reducible] [unfold-f] (a : A) : A := +definition id [reducible] [unfold-full] (a : A) : A := a -definition on_fun [reducible] [unfold-f] (f : B → B → C) (g : A → B) : A → A → C := +definition on_fun [reducible] [unfold-full] (f : B → B → C) (g : A → B) : A → A → C := λx y, f (g x) (g y) -definition combine [reducible] [unfold-f] (f : A → B → C) (op : C → D → E) (g : A → B → D) +definition combine [reducible] [unfold-full] (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E := λx y, op (f x y) (g x y) -definition const [reducible] [unfold-f] (B : Type) (a : A) : B → A := +definition const [reducible] [unfold-full] (B : Type) (a : A) : B → A := λx, a -definition dcompose [reducible] [unfold-f] {B : A → Type} {C : Π {x : A}, B x → Type} +definition dcompose [reducible] [unfold-full] {B : A → Type} {C : Π {x : A}, B x → Type} (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) := λx, f (g x) -definition flip [reducible] [unfold-f] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y := +definition flip [reducible] [unfold-full] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y := λy x, f x y -definition app [reducible] [unfold-f] {B : A → Type} (f : Πx, B x) (x : A) : B x := +definition app [reducible] [unfold-full] {B : A → Type} (f : Πx, B x) (x : A) : B x := f x -definition curry [reducible] [unfold-f] : (A × B → C) → A → B → C := +definition curry [reducible] [unfold-full] : (A × B → C) → A → B → C := λ f a b, f (a, b) -definition uncurry [reducible] [unfold-c 5] : (A → B → C) → (A × B → C) := +definition uncurry [reducible] [unfold 5] : (A → B → C) → (A × B → C) := λ f p, match p with (a, b) := f a b end precedence `∘'`:60 diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean index 83bf7113c..36105c262 100644 --- a/hott/init/hit.hlean +++ b/hott/init/hit.hlean @@ -85,5 +85,5 @@ namespace quotient end quotient attribute quotient.class_of trunc.tr [constructor] -attribute quotient.rec trunc.rec [unfold-c 6] -attribute quotient.rec_on trunc.rec_on [unfold-c 4] +attribute quotient.rec trunc.rec [unfold 6] +attribute quotient.rec_on trunc.rec_on [unfold 4] diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index 65f7ead77..af1ea7d8a 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -42,13 +42,13 @@ definition rfl {A : Type} {a : A} := eq.refl a namespace eq variables {A : Type} {a b c : A} - definition subst [unfold-c 5] {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b := + definition subst [unfold 5] {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b := eq.rec H₂ H₁ - definition trans [unfold-c 5] (H₁ : a = b) (H₂ : b = c) : a = c := + definition trans [unfold 5] (H₁ : a = b) (H₂ : b = c) : a = c := subst H₂ H₁ - definition symm [unfold-c 4] (H : a = b) : b = a := + definition symm [unfold 4] (H : a = b) : b = a := subst H (refl a) namespace ops diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index 2657dfdd3..19953fb4f 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -26,7 +26,7 @@ namespace nat infix `≥` := ge infix `>` := gt - definition pred [unfold-c 1] (a : nat) : nat := + definition pred [unfold 1] (a : nat) : nat := nat.cases_on a zero (λ a₁, a₁) -- add is defined in init.num @@ -73,16 +73,16 @@ namespace nat definition le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H - definition succ_le_succ [unfold-c 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := + definition succ_le_succ [unfold 3] {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := by induction H;reflexivity;exact le.step v_0 - definition pred_le_pred [unfold-c 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m := + definition pred_le_pred [unfold 3] {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m := by induction H;reflexivity;cases b;exact v_0;exact le.step v_0 - definition le_of_succ_le_succ [unfold-c 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m := + definition le_of_succ_le_succ [unfold 3] {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m := pred_le_pred H - definition le_succ_of_pred_le [unfold-c 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m := + definition le_succ_of_pred_le [unfold 1] {n m : ℕ} (H : pred n ≤ m) : n ≤ succ m := by cases n;exact le.step H;exact succ_le_succ H definition not_succ_le_self {n : ℕ} : ¬succ n ≤ n := diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 4c7778404..81f31f54d 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -22,20 +22,20 @@ namespace eq definition idpath [reducible] [constructor] (a : A) := refl a -- unbased path induction - definition rec' [reducible] [unfold-c 6] {P : Π (a b : A), (a = b) → Type} + definition rec' [reducible] [unfold 6] {P : Π (a b : A), (a = b) → Type} (H : Π (a : A), P a a idp) {a b : A} (p : a = b) : P a b p := eq.rec (H a) p - definition rec_on' [reducible] [unfold-c 5] {P : Π (a b : A), (a = b) → Type} + definition rec_on' [reducible] [unfold 5] {P : Π (a b : A), (a = b) → Type} {a b : A} (p : a = b) (H : Π (a : A), P a a idp) : P a b p := eq.rec (H a) p /- Concatenation and inverse -/ - definition concat [trans] [unfold-c 6] (p : x = y) (q : y = z) : x = z := + definition concat [trans] [unfold 6] (p : x = y) (q : y = z) : x = z := eq.rec (λp', p') q p - definition inverse [symm] [unfold-c 4] (p : x = y) : y = x := + definition inverse [symm] [unfold 4] (p : x = y) : y = x := eq.rec (refl x) p infix ⬝ := concat @@ -46,11 +46,11 @@ namespace eq /- The 1-dimensional groupoid structure -/ -- The identity path is a right unit. - definition con_idp [unfold-f] (p : x = y) : p ⬝ idp = p := + definition con_idp [unfold-full] (p : x = y) : p ⬝ idp = p := idp -- The identity path is a right unit. - definition idp_con [unfold-c 4] (p : x = y) : idp ⬝ p = p := + definition idp_con [unfold 4] (p : x = y) : idp ⬝ p = p := eq.rec_on p idp -- Concatenation is associative. @@ -63,11 +63,11 @@ namespace eq eq.rec_on r (eq.rec_on q idp) -- The left inverse law. - definition con.right_inv [unfold-c 4] (p : x = y) : p ⬝ p⁻¹ = idp := + definition con.right_inv [unfold 4] (p : x = y) : p ⬝ p⁻¹ = idp := eq.rec_on p idp -- The right inverse law. - definition con.left_inv [unfold-c 4] (p : x = y) : p⁻¹ ⬝ p = idp := + definition con.left_inv [unfold 4] (p : x = y) : p⁻¹ ⬝ p = idp := eq.rec_on p idp /- Several auxiliary theorems about canceling inverses across associativity. These are somewhat @@ -113,7 +113,7 @@ namespace eq p = r⁻¹ ⬝ q → r ⬝ p = q := eq.rec_on r (take p h, !idp_con ⬝ h ⬝ !idp_con) p - definition con_eq_of_eq_con_inv [unfold-c 5] {p : x = z} {q : y = z} {r : y = x} : + definition con_eq_of_eq_con_inv [unfold 5] {p : x = z} {q : y = z} {r : y = x} : r = q ⬝ p⁻¹ → r ⬝ p = q := eq.rec_on p (take q h, h) q @@ -121,7 +121,7 @@ namespace eq p = r ⬝ q → r⁻¹ ⬝ p = q := eq.rec_on r (take q h, !idp_con ⬝ h ⬝ !idp_con) q - definition con_inv_eq_of_eq_con [unfold-c 5] {p : z = x} {q : y = z} {r : y = x} : + definition con_inv_eq_of_eq_con [unfold 5] {p : z = x} {q : y = z} {r : y = x} : r = q ⬝ p → r ⬝ p⁻¹ = q := eq.rec_on p (take r h, h) r @@ -129,7 +129,7 @@ namespace eq r⁻¹ ⬝ q = p → q = r ⬝ p := eq.rec_on r (take p h, !idp_con⁻¹ ⬝ h ⬝ !idp_con⁻¹) p - definition eq_con_of_con_inv_eq [unfold-c 5] {p : x = z} {q : y = z} {r : y = x} : + definition eq_con_of_con_inv_eq [unfold 5] {p : x = z} {q : y = z} {r : y = x} : q ⬝ p⁻¹ = r → q = r ⬝ p := eq.rec_on p (take q h, h) q @@ -137,17 +137,17 @@ namespace eq r ⬝ q = p → q = r⁻¹ ⬝ p := eq.rec_on r (take q h, !idp_con⁻¹ ⬝ h ⬝ !idp_con⁻¹) q - definition eq_con_inv_of_con_eq [unfold-c 5] {p : z = x} {q : y = z} {r : y = x} : + definition eq_con_inv_of_con_eq [unfold 5] {p : z = x} {q : y = z} {r : y = x} : q ⬝ p = r → q = r ⬝ p⁻¹ := eq.rec_on p (take r h, h) r - definition eq_of_con_inv_eq_idp [unfold-c 5] {p q : x = y} : p ⬝ q⁻¹ = idp → p = q := + definition eq_of_con_inv_eq_idp [unfold 5] {p q : x = y} : p ⬝ q⁻¹ = idp → p = q := eq.rec_on q (take p h, h) p definition eq_of_inv_con_eq_idp {p q : x = y} : q⁻¹ ⬝ p = idp → p = q := eq.rec_on q (take p h, !idp_con⁻¹ ⬝ h) p - definition eq_inv_of_con_eq_idp' [unfold-c 5] {p : x = y} {q : y = x} : p ⬝ q = idp → p = q⁻¹ := + definition eq_inv_of_con_eq_idp' [unfold 5] {p : x = y} {q : y = x} : p ⬝ q = idp → p = q⁻¹ := eq.rec_on q (take p h, h) p definition eq_inv_of_con_eq_idp {p : x = y} {q : y = x} : q ⬝ p = idp → p = q⁻¹ := @@ -156,10 +156,10 @@ namespace eq definition eq_of_idp_eq_inv_con {p q : x = y} : idp = p⁻¹ ⬝ q → p = q := eq.rec_on p (take q h, h ⬝ !idp_con) q - definition eq_of_idp_eq_con_inv [unfold-c 4] {p q : x = y} : idp = q ⬝ p⁻¹ → p = q := + definition eq_of_idp_eq_con_inv [unfold 4] {p q : x = y} : idp = q ⬝ p⁻¹ → p = q := eq.rec_on p (take q h, h) q - definition inv_eq_of_idp_eq_con [unfold-c 4] {p : x = y} {q : y = x} : idp = q ⬝ p → p⁻¹ = q := + definition inv_eq_of_idp_eq_con [unfold 4] {p : x = y} {q : y = x} : idp = q ⬝ p → p⁻¹ = q := eq.rec_on p (take q h, h) q definition inv_eq_of_idp_eq_con' {p : x = y} {q : y = x} : idp = p ⬝ q → p⁻¹ = q := @@ -185,20 +185,20 @@ namespace eq /- Transport -/ - definition transport [subst] [reducible] [unfold-c 5] (P : A → Type) {x y : A} (p : x = y) + definition transport [subst] [reducible] [unfold 5] (P : A → Type) {x y : A} (p : x = y) (u : P x) : P y := eq.rec_on p u -- This idiom makes the operation right associative. notation p `▸` x := transport _ p x - definition cast [reducible] [unfold-c 3] {A B : Type} (p : A = B) (a : A) : B := + definition cast [reducible] [unfold 3] {A B : Type} (p : A = B) (a : A) : B := p ▸ a - definition tr_rev [reducible] [unfold-c 6] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x := + definition tr_rev [reducible] [unfold 6] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x := p⁻¹ ▸ u - definition ap [unfold-c 6] ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x = y) : f x = f y := + definition ap [unfold 6] ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x = y) : f x = f y := eq.rec_on p idp abbreviation ap01 [parsing-only] := ap @@ -218,19 +218,19 @@ namespace eq (H1 : f ~ g) (H2 : g ~ h) : f ~ h := λ x, H1 x ⬝ H2 x - definition apd10 [unfold-c 5] {f g : Πx, P x} (H : f = g) : f ~ g := + definition apd10 [unfold 5] {f g : Πx, P x} (H : f = g) : f ~ g := λx, eq.rec_on H idp --the next theorem is useful if you want to write "apply (apd10' a)" - definition apd10' [unfold-c 6] {f g : Πx, P x} (a : A) (H : f = g) : f a = g a := + definition apd10' [unfold 6] {f g : Πx, P x} (a : A) (H : f = g) : f a = g a := eq.rec_on H idp - definition ap10 [reducible] [unfold-c 5] {f g : A → B} (H : f = g) : f ~ g := apd10 H + definition ap10 [reducible] [unfold 5] {f g : A → B} (H : f = g) : f ~ g := apd10 H definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y := eq.rec_on H (eq.rec_on p idp) - definition apd [unfold-c 6] (f : Πa, P a) {x y : A} (p : x = y) : p ▸ f x = f y := + definition apd [unfold 6] (f : Πa, P a) {x y : A} (p : x = y) : p ▸ f x = f y := eq.rec_on p idp /- More theorems for moving things around in equations -/ @@ -294,7 +294,7 @@ namespace eq eq.rec_on p idp -- The action of constant maps. - definition ap_constant [unfold-c 5] (p : x = y) (z : B) : ap (λu, z) p = idp := + definition ap_constant [unfold 5] (p : x = y) (z : B) : ap (λu, z) p = idp := eq.rec_on p idp -- Naturality of [ap]. @@ -443,7 +443,7 @@ namespace eq -- Dependent transport in a doubly dependent type. - definition transportD [unfold-c 6] {P : A → Type} (Q : Πa, P a → Type) + definition transportD [unfold 6] {P : A → Type} (Q : Πa, P a → Type) {a a' : A} (p : a = a') (b : P a) (z : Q a b) : Q a' (p ▸ b) := eq.rec_on p z @@ -452,7 +452,7 @@ namespace eq notation p `▸D`:65 x:64 := transportD _ p _ x -- Transporting along higher-dimensional paths - definition transport2 [unfold-c 7] (P : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : P x) : + definition transport2 [unfold 7] (P : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : P x) : p ▸ z = q ▸ z := ap (λp', p' ▸ z) r @@ -473,7 +473,7 @@ namespace eq transport2 Q r⁻¹ z = (transport2 Q r z)⁻¹ := eq.rec_on r idp - definition transportD2 [unfold-c 7] (B C : A → Type) (D : Π(a:A), B a → C a → Type) + definition transportD2 [unfold 7] (B C : A → Type) (D : Π(a:A), B a → C a → Type) {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▸ y) (p ▸ z) := eq.rec_on p w @@ -549,7 +549,7 @@ namespace eq eq.rec_on h (eq.rec_on h' idp) -- 2-dimensional path inversion - definition inverse2 [unfold-c 6] {p q : x = y} (h : p = q) : p⁻¹ = q⁻¹ := + definition inverse2 [unfold 6] {p q : x = y} (h : p = q) : p⁻¹ = q⁻¹ := eq.rec_on h idp infixl `◾`:75 := concat2 @@ -631,7 +631,7 @@ namespace eq ⬝ (!whisker_left_idp_left ◾ !whisker_right_idp_right) -- The action of functions on 2-dimensional paths - definition ap02 [unfold-c 8] [reducible] (f : A → B) {x y : A} {p q : x = y} (r : p = q) + definition ap02 [unfold 8] [reducible] (f : A → B) {x y : A} {p q : x = y} (r : p = q) : ap f p = ap f q := ap (ap f) r @@ -646,7 +646,7 @@ namespace eq ⬝ (ap_con f p' q')⁻¹ := eq.rec_on r (eq.rec_on s (eq.rec_on q (eq.rec_on p idp))) - definition apd02 [unfold-c 8] {p q : x = y} (f : Π x, P x) (r : p = q) : + definition apd02 [unfold 8] {p q : x = y} (f : Π x, P x) (r : p = q) : apd f p = transport2 P r (f x) ⬝ apd f q := eq.rec_on r !idp_con⁻¹ diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index 52ec74fc0..d3ead5838 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -32,10 +32,10 @@ namespace eq definition pathover_of_eq_tr (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ := by cases p; cases r; exact idpo - definition tr_eq_of_pathover [unfold-c 8] (r : b =[p] b₂) : p ▸ b = b₂ := + definition tr_eq_of_pathover [unfold 8] (r : b =[p] b₂) : p ▸ b = b₂ := by cases r; exact idp - definition eq_tr_of_pathover [unfold-c 8] (r : b =[p] b₂) : b = p⁻¹ ▸ b₂ := + definition eq_tr_of_pathover [unfold 8] (r : b =[p] b₂) : b = p⁻¹ ▸ b₂ := by cases r; exact idp definition pathover_equiv_tr_eq [constructor] (p : a = a₂) (b : B a) (b₂ : B a₂) @@ -58,28 +58,28 @@ namespace eq { intro r, cases r, apply idp}, end - definition pathover_tr [unfold-c 5] (p : a = a₂) (b : B a) : b =[p] p ▸ b := + definition pathover_tr [unfold 5] (p : a = a₂) (b : B a) : b =[p] p ▸ b := by cases p;exact idpo - definition tr_pathover [unfold-c 5] (p : a = a₂) (b : B a₂) : p⁻¹ ▸ b =[p] b := + definition tr_pathover [unfold 5] (p : a = a₂) (b : B a₂) : p⁻¹ ▸ b =[p] b := pathover_of_eq_tr idp - definition concato [unfold-c 12] (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ := + definition concato [unfold 12] (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ := pathover.rec_on r₂ r - definition inverseo [unfold-c 8] (r : b =[p] b₂) : b₂ =[p⁻¹] b := + definition inverseo [unfold 8] (r : b =[p] b₂) : b₂ =[p⁻¹] b := pathover.rec_on r idpo - definition apdo [unfold-c 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ := + definition apdo [unfold 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ := eq.rec_on p idpo - definition oap [unfold-c 6] {C : A → Type} (f : Πa, B a → C a) (p : a = a₂) : f a =[p] f a₂ := + definition oap [unfold 6] {C : A → Type} (f : Πa, B a → C a) (p : a = a₂) : f a =[p] f a₂ := eq.rec_on p idpo - definition concato_eq [unfold-c 10] (r : b =[p] b₂) (q : b₂ = b₂') : b =[p] b₂' := + definition concato_eq [unfold 10] (r : b =[p] b₂) (q : b₂ = b₂') : b =[p] b₂' := eq.rec_on q r - definition eq_concato [unfold-c 9] (q : b = b') (r : b' =[p] b₂) : b =[p] b₂ := + definition eq_concato [unfold 9] (q : b = b') (r : b' =[p] b₂) : b =[p] b₂ := by induction q;exact r -- infix `⬝` := concato @@ -126,11 +126,11 @@ namespace eq { intro r, cases r, exact idp}, end - definition eq_of_pathover_idp [unfold-c 6] {b' : B a} (q : b =[idpath a] b') : b = b' := + definition eq_of_pathover_idp [unfold 6] {b' : B a} (q : b =[idpath a] b') : b = b' := tr_eq_of_pathover q --should B be explicit in the next two definitions? - definition pathover_idp_of_eq [unfold-c 6] {b' : B a} (q : b = b') : b =[idpath a] b' := + definition pathover_idp_of_eq [unfold 6] {b' : B a} (q : b = b') : b =[idpath a] b' := eq.rec_on q idpo definition pathover_idp [constructor] (b : B a) (b' : B a) : b =[idpath a] b' ≃ b = b' := @@ -164,7 +164,7 @@ namespace eq by cases r; exact H --pathover with fibration B' ∘ f - definition pathover_ap [unfold-c 10] (B' : A' → Type) (f : A → A') {p : a = a₂} + definition pathover_ap [unfold 10] (B' : A' → Type) (f : A → A') {p : a = a₂} {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[p] b₂) : b =[ap f p] b₂ := by cases q; exact idpo diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 6bd67e46e..68fcd3a1b 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -261,7 +261,7 @@ namespace is_trunc (f : A → B) (g : B → A) : A ≃ B := equiv.mk f (is_equiv_of_is_hprop f g) - definition equiv_of_iff_of_is_hprop [unfold-c 5] [HA : is_hprop A] [HB : is_hprop B] (H : A ↔ B) : A ≃ B := + definition equiv_of_iff_of_is_hprop [unfold 5] [HA : is_hprop A] [HB : is_hprop B] (H : A ↔ B) : A ≃ B := equiv_of_is_hprop (iff.elim_left H) (iff.elim_right H) end diff --git a/hott/types/W.hlean b/hott/types/W.hlean index 44a682c6b..fa074a905 100644 --- a/hott/types/W.hlean +++ b/hott/types/W.hlean @@ -19,10 +19,10 @@ namespace Wtype variables {A A' : Type.{u}} {B B' : A → Type.{v}} {C : Π(a : A), B a → Type} {a a' : A} {f : B a → W a, B a} {f' : B a' → W a, B a} {w w' : W(a : A), B a} - protected definition pr1 [unfold-c 3] (w : W(a : A), B a) : A := + protected definition pr1 [unfold 3] (w : W(a : A), B a) : A := by cases w with a f; exact a - protected definition pr2 [unfold-c 3] (w : W(a : A), B a) : B (Wtype.pr1 w) → W(a : A), B a := + protected definition pr2 [unfold 3] (w : W(a : A), B a) : B (Wtype.pr1 w) → W(a : A), B a := by cases w with a f; exact f namespace ops diff --git a/hott/types/cubical/square.hlean b/hott/types/cubical/square.hlean index 36d692c9f..cb279f8fc 100644 --- a/hott/types/cubical/square.hlean +++ b/hott/types/cubical/square.hlean @@ -29,50 +29,50 @@ namespace eq definition ids [reducible] [constructor] := @square.ids definition idsquare [reducible] [constructor] (a : A) := @square.ids A a - definition hrefl [unfold-c 4] (p : a = a') : square idp idp p p := + definition hrefl [unfold 4] (p : a = a') : square idp idp p p := by induction p; exact ids - definition vrefl [unfold-c 4] (p : a = a') : square p p idp idp := + definition vrefl [unfold 4] (p : a = a') : square p p idp idp := by induction p; exact ids - definition hrfl [unfold-c 4] {p : a = a'} : square idp idp p p := + definition hrfl [unfold 4] {p : a = a'} : square idp idp p p := !hrefl - definition vrfl [unfold-c 4] {p : a = a'} : square p p idp idp := + definition vrfl [unfold 4] {p : a = a'} : square p p idp idp := !vrefl - definition hdeg_square [unfold-c 6] {p q : a = a'} (r : p = q) : square idp idp p q := + definition hdeg_square [unfold 6] {p q : a = a'} (r : p = q) : square idp idp p q := by induction r;apply hrefl - definition vdeg_square [unfold-c 6] {p q : a = a'} (r : p = q) : square p q idp idp := + definition vdeg_square [unfold 6] {p q : a = a'} (r : p = q) : square p q idp idp := by induction r;apply vrefl - definition hconcat [unfold-c 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁) + definition hconcat [unfold 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁) : square (p₁₀ ⬝ p₃₀) (p₁₂ ⬝ p₃₂) p₀₁ p₄₁ := by induction s₃₁; exact s₁₁ - definition vconcat [unfold-c 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃) + definition vconcat [unfold 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃) : square p₁₀ p₁₄ (p₀₁ ⬝ p₀₃) (p₂₁ ⬝ p₂₃) := by induction s₁₃; exact s₁₁ - definition hinverse [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀⁻¹ p₁₂⁻¹ p₂₁ p₀₁ := + definition hinverse [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀⁻¹ p₁₂⁻¹ p₂₁ p₀₁ := by induction s₁₁;exact ids - definition vinverse [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₂ p₁₀ p₀₁⁻¹ p₂₁⁻¹ := + definition vinverse [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₂ p₁₀ p₀₁⁻¹ p₂₁⁻¹ := by induction s₁₁;exact ids - definition eq_vconcat [unfold-c 11] {p : a₀₀ = a₂₀} (r : p = p₁₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : + definition eq_vconcat [unfold 11] {p : a₀₀ = a₂₀} (r : p = p₁₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p p₁₂ p₀₁ p₂₁ := by induction r; exact s₁₁ - definition vconcat_eq [unfold-c 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) : + definition vconcat_eq [unfold 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) : square p₁₀ p p₀₁ p₂₁ := by induction r; exact s₁₁ - definition eq_hconcat [unfold-c 11] {p : a₀₀ = a₀₂} (r : p = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : + definition eq_hconcat [unfold 11] {p : a₀₀ = a₀₂} (r : p = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀ p₁₂ p p₂₁ := by induction r; exact s₁₁ - definition hconcat_eq [unfold-c 11] {p : a₂₀ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) : + definition hconcat_eq [unfold 11] {p : a₂₀ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) : square p₁₀ p₁₂ p₀₁ p := by induction r; exact s₁₁ @@ -86,18 +86,18 @@ namespace eq postfix `⁻¹ʰ`:(max+1) := hinverse postfix `⁻¹ᵛ`:(max+1) := vinverse - definition transpose [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₀₁ p₂₁ p₁₀ p₁₂ := + definition transpose [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₀₁ p₂₁ p₁₀ p₁₂ := by induction s₁₁;exact ids definition aps {B : Type} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square (ap f p₁₀) (ap f p₁₂) (ap f p₀₁) (ap f p₂₁) := by induction s₁₁;exact ids - definition natural_square [unfold-c 8] {f g : A → B} (p : f ~ g) (q : a = a') : + definition natural_square [unfold 8] {f g : A → B} (p : f ~ g) (q : a = a') : square (ap f q) (ap g q) (p a) (p a') := eq.rec_on q hrfl - definition natural_square_tr [unfold-c 8] {f g : A → B} (p : f ~ g) (q : a = a') : + definition natural_square_tr [unfold 8] {f g : A → B} (p : f ~ g) (q : a = a') : square (p a) (p a') (ap f q) (ap g q) := eq.rec_on q vrfl @@ -121,13 +121,13 @@ namespace eq /- equivalences -/ - definition eq_of_square [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂ := + definition eq_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂ := by induction s₁₁; apply idp definition square_of_eq (r : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : square p₁₀ p₁₂ p₀₁ p₂₁ := by induction p₁₂; esimp [concat] at r; induction r; induction p₂₁; induction p₁₀; exact ids - definition eq_top_of_square [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + definition eq_top_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ = p₀₁ ⬝ p₁₂ ⬝ p₂₁⁻¹ := by induction s₁₁; apply idp @@ -186,11 +186,11 @@ namespace eq -- example (p q : a = a') : to_inv (hdeg_square_equiv' p q) = hdeg_square := idp -- this fails example (p q : a = a') : to_inv (hdeg_square_equiv p q) = hdeg_square := idp - definition pathover_eq [unfold-c 7] {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'} + definition pathover_eq [unfold 7] {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'} (s : square q r (ap f p) (ap g p)) : q =[p] r := by induction p;apply pathover_idp_of_eq;exact eq_of_vdeg_square s - definition square_of_pathover [unfold-c 7] + definition square_of_pathover [unfold 7] {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'} (s : q =[p] r) : square q r (ap f p) (ap g p) := by induction p;apply vdeg_square;exact eq_of_pathover_idp s @@ -253,15 +253,15 @@ namespace eq by induction s₁₁; induction r;reflexivity - -- definition vconcat_eq [unfold-c 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) : + -- definition vconcat_eq [unfold 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) : -- square p₁₀ p p₀₁ p₂₁ := -- by induction r; exact s₁₁ - -- definition eq_hconcat [unfold-c 11] {p : a₀₀ = a₀₂} (r : p = p₀₁) + -- definition eq_hconcat [unfold 11] {p : a₀₀ = a₀₂} (r : p = p₀₁) -- (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀ p₁₂ p p₂₁ := -- by induction r; exact s₁₁ - -- definition hconcat_eq [unfold-c 11] {p : a₂₀ = a₂₂} + -- definition hconcat_eq [unfold 11] {p : a₂₀ = a₂₂} -- (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) : square p₁₀ p₁₂ p₀₁ p := -- by induction r; exact s₁₁ diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index ebac2f48f..f53196dc7 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -90,7 +90,7 @@ namespace eq theorem idp_con_idp {p : a = a} (q : p = idp) : idp_con p ⬝ q = ap (λp, idp ⬝ p) q := by cases q;reflexivity - definition ap_weakly_constant [unfold-c 8] {A B : Type} {f : A → B} {b : B} (p : Πx, f x = b) + definition ap_weakly_constant [unfold 8] {A B : Type} {f : A → B} {b : B} (p : Πx, f x = b) {x y : A} (q : x = y) : ap f q = p x ⬝ (p y)⁻¹ := by induction q;exact !con.right_inv⁻¹ diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean index 21bfdd81b..2e7f123c8 100644 --- a/hott/types/int/basic.hlean +++ b/hott/types/int/basic.hlean @@ -797,7 +797,7 @@ definition pred_nat_succ (n : ℕ) : pred (nat.succ n) = n := pred_succ n definition neg_nat_succ (n : ℕ) : -nat.succ n = pred (-n) := !neg_succ definition succ_neg_nat_succ (n : ℕ) : succ (-nat.succ n) = -n := !succ_neg_succ -definition rec_nat_on [unfold-c 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) +definition rec_nat_on [unfold 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) (Hpred : Π⦃n : ℕ⦄, P (-n) → P (-nat.succ n)) : P z := begin induction z with n n, diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index cbbf7ad15..1de0449ae 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -22,7 +22,7 @@ namespace pointed attribute Pointed.carrier [coercion] variables {A B : Type} - definition pt [unfold-c 2] [H : pointed A] := point A + definition pt [unfold 2] [H : pointed A] := point A protected abbreviation Mk [constructor] := @Pointed.mk protected definition mk' [constructor] (A : Type) [H : pointed A] : Pointed := Pointed.mk (point A) @@ -100,7 +100,7 @@ open pmap namespace pointed - abbreviation respect_pt [unfold-c 3] := @pmap.resp_pt + abbreviation respect_pt [unfold 3] := @pmap.resp_pt notation `map₊` := pmap infix `→*`:30 := pmap attribute pmap.map [coercion] @@ -129,8 +129,8 @@ namespace pointed (homotopy_pt : homotopy pt ⬝ respect_pt g = respect_pt f) infix `~*`:50 := phomotopy - abbreviation to_homotopy_pt [unfold-c 5] := @phomotopy.homotopy_pt - abbreviation to_homotopy [coercion] [unfold-c 5] (p : f ~* g) : Πa, f a = g a := + abbreviation to_homotopy_pt [unfold 5] := @phomotopy.homotopy_pt + abbreviation to_homotopy [coercion] [unfold 5] (p : f ~* g) : Πa, f a = g a := phomotopy.homotopy p definition passoc (h : C →* D) (g : B →* C) (f : A →* B) : (h ∘* g) ∘* f ~* h ∘* (g ∘* f) := diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 0710de320..4ae941aa3 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -196,7 +196,7 @@ namespace sigma /- Functorial action -/ variables (f : A → A') (g : Πa, B a → B' (f a)) - definition sigma_functor [unfold-c 7] (u : Σa, B a) : Σa', B' a' := + definition sigma_functor [unfold 7] (u : Σa, B a) : Σa', B' a' := ⟨f u.1, g u.1 u.2⟩ /- Equivalences -/ diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 12963345c..2f0b18c75 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -664,7 +664,7 @@ theorem pred_nat_succ (n : ℕ) : pred (nat.succ n) = n := pred_succ n theorem neg_nat_succ (n : ℕ) : -nat.succ n = pred (-n) := !neg_succ theorem succ_neg_nat_succ (n : ℕ) : succ (-nat.succ n) = -n := !succ_neg_succ -definition rec_nat_on [unfold-c 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) +definition rec_nat_on [unfold 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) (Hpred : Π⦃n : ℕ⦄, P (-n) → P (-nat.succ n)) : P z := begin induction z with n n, diff --git a/library/data/stream.lean b/library/data/stream.lean index 513720dce..1793a2216 100644 --- a/library/data/stream.lean +++ b/library/data/stream.lean @@ -282,7 +282,7 @@ definition unfolds (g : A → B) (f : A → A) (a : A) : stream B := corec g f a theorem unfolds_eq (g : A → B) (f : A → A) (a : A) : unfolds g f a = g a :: unfolds g f (f a) := -by esimp [unfolds]; rewrite [corec_eq] +by esimp [ unfolds ]; rewrite [corec_eq] theorem nth_unfolds_head_tail : ∀ (n : nat) (s : stream A), nth n (unfolds head tail s) = nth n s := begin diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index 9c0cad91e..58cc893bb 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -38,10 +38,10 @@ refl : heq a a inductive prod (A B : Type) := mk : A → B → prod A B -definition prod.pr1 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : A := +definition prod.pr1 [reducible] [unfold 3] {A B : Type} (p : prod A B) : A := prod.rec (λ a b, a) p -definition prod.pr2 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : B := +definition prod.pr2 [reducible] [unfold 3] {A B : Type} (p : prod A B) : B := prod.rec (λ a b, b) p inductive and (a b : Prop) : Prop := diff --git a/library/init/function.lean b/library/init/function.lean index e8cef46a8..2a8d28684 100644 --- a/library/init/function.lean +++ b/library/init/function.lean @@ -12,42 +12,42 @@ namespace function variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type} -definition compose [reducible] [unfold-f] (f : B → C) (g : A → B) : A → C := +definition compose [reducible] [unfold-full] (f : B → C) (g : A → B) : A → C := λx, f (g x) -definition compose_right [reducible] [unfold-f] (f : B → B → B) (g : A → B) : B → A → B := +definition compose_right [reducible] [unfold-full] (f : B → B → B) (g : A → B) : B → A → B := λ b a, f b (g a) -definition compose_left [reducible] [unfold-f] (f : B → B → B) (g : A → B) : A → B → B := +definition compose_left [reducible] [unfold-full] (f : B → B → B) (g : A → B) : A → B → B := λ a b, f (g a) b -definition id [reducible] [unfold-f] (a : A) : A := +definition id [reducible] [unfold-full] (a : A) : A := a -definition on_fun [reducible] [unfold-f] (f : B → B → C) (g : A → B) : A → A → C := +definition on_fun [reducible] [unfold-full] (f : B → B → C) (g : A → B) : A → A → C := λx y, f (g x) (g y) -definition combine [reducible] [unfold-f] (f : A → B → C) (op : C → D → E) (g : A → B → D) +definition combine [reducible] [unfold-full] (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E := λx y, op (f x y) (g x y) -definition const [reducible] [unfold-f] (B : Type) (a : A) : B → A := +definition const [reducible] [unfold-full] (B : Type) (a : A) : B → A := λx, a -definition dcompose [reducible] [unfold-f] {B : A → Type} {C : Π {x : A}, B x → Type} +definition dcompose [reducible] [unfold-full] {B : A → Type} {C : Π {x : A}, B x → Type} (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) := λx, f (g x) -definition swap [reducible] [unfold-f] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y := +definition swap [reducible] [unfold-full] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y := λy x, f x y definition app [reducible] {B : A → Type} (f : Πx, B x) (x : A) : B x := f x -definition curry [reducible] [unfold-f] : (A × B → C) → A → B → C := +definition curry [reducible] [unfold-full] : (A × B → C) → A → B → C := λ f a b, f (a, b) -definition uncurry [reducible] [unfold-c 5] : (A → B → C) → (A × B → C) := +definition uncurry [reducible] [unfold 5] : (A → B → C) → (A × B → C) := λ f p, match p with (a, b) := f a b end theorem curry_uncurry (f : A → B → C) : curry (uncurry f) = f := diff --git a/library/init/nat.lean b/library/init/nat.lean index f7b0c3b88..c44290f8e 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -25,7 +25,7 @@ namespace nat infix `≥` := ge infix `>` := gt - definition pred [unfold-c 1] (a : nat) : nat := + definition pred [unfold 1] (a : nat) : nat := nat.cases_on a zero (λ a₁, a₁) -- add is defined in init.num diff --git a/library/init/quot.lean b/library/init/quot.lean index 1e3b93c6b..c28104ace 100644 --- a/library/init/quot.lean +++ b/library/init/quot.lean @@ -164,15 +164,15 @@ namespace quot end quot attribute quot.mk [constructor] -attribute quot.lift_on [unfold-c 4] -attribute quot.rec [unfold-c 6] -attribute quot.rec_on [unfold-c 4] -attribute quot.hrec_on [unfold-c 4] -attribute quot.rec_on_subsingleton [unfold-c 5] -attribute quot.lift₂ [unfold-c 8] -attribute quot.lift_on₂ [unfold-c 6] -attribute quot.hrec_on₂ [unfold-c 6] -attribute quot.rec_on_subsingleton₂ [unfold-c 7] +attribute quot.lift_on [unfold 4] +attribute quot.rec [unfold 6] +attribute quot.rec_on [unfold 4] +attribute quot.hrec_on [unfold 4] +attribute quot.rec_on_subsingleton [unfold 5] +attribute quot.lift₂ [unfold 8] +attribute quot.lift_on₂ [unfold 6] +attribute quot.hrec_on₂ [unfold 6] +attribute quot.rec_on_subsingleton₂ [unfold 7] open decidable definition quot.has_decidable_eq [instance] {A : Type} {s : setoid A} [decR : ∀ a b : A, decidable (a ≈ b)] : decidable_eq (quot s) := diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 67e55da1a..ee42d8c40 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -119,7 +119,7 @@ (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face) ;; modifiers (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[trans-instance\]" "\[class\]" "\[parsing-only\]" - "\[coercion\]" "\[unfold-f\]" "\[constructor\]" "\[reducible\]" + "\[coercion\]" "\[unfold-full\]" "\[constructor\]" "\[reducible\]" "\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]" "\[none\]" "\[decls\]" "\[declarations\]" "\[coercions\]" "\[classes\]" @@ -129,7 +129,7 @@ . 'font-lock-doc-face) (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) (,(rx "\[recursor" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) - (,(rx "\[unfold-c" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) + (,(rx "\[unfold" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) ;; tactics ("cases[ \t\n]+[^ \t\n]+[ \t\n]+\\(with\\)" (1 'font-lock-constant-face)) (,(rx (not (any "\.")) word-start diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 845ad7102..34fa28afb 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -670,6 +670,10 @@ environment set_option_cmd(parser & p) { return update_fingerprint(env, p.get_options().hash()); } +static bool is_next_metaclass_tk(parser const & p) { + return p.curr_is_token(get_lbracket_tk()) || p.curr_is_token(get_unfold_hints_bracket_tk()); +} + static name parse_metaclass(parser & p) { if (p.curr_is_token(get_lbracket_tk())) { p.next(); @@ -690,6 +694,9 @@ static name parse_metaclass(parser & p) { if (!is_metaclass(n) && n != get_decls_tk() && n != get_declarations_tk()) throw parser_error(sstream() << "invalid metaclass name '[" << n << "]'", pos); return n; + } else if (p.curr_is_token(get_unfold_hints_bracket_tk())) { + p.next(); + return get_unfold_hints_tk(); } else { return name(); } @@ -701,7 +708,7 @@ static void parse_metaclasses(parser & p, buffer & r) { buffer tmp; get_metaclasses(tmp); tmp.push_back(get_decls_tk()); - while (p.curr_is_token(get_lbracket_tk())) { + while (is_next_metaclass_tk(p)) { name m = parse_metaclass(p); tmp.erase_elem(m); if (m == get_declarations_tk()) @@ -709,7 +716,7 @@ static void parse_metaclasses(parser & p, buffer & r) { } r.append(tmp); } else { - while (p.curr_is_token(get_lbracket_tk())) { + while (is_next_metaclass_tk(p)) { r.push_back(parse_metaclass(p)); } } @@ -837,7 +844,7 @@ environment open_export_cmd(parser & p, bool open) { } } } - if (!p.curr_is_token(get_lbracket_tk()) && !p.curr_is_identifier()) + if (!is_next_metaclass_tk(p) && !p.curr_is_identifier()) break; } return update_fingerprint(env, fingerprint); diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 7cff97bb5..43c620ea6 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -32,7 +32,7 @@ decl_attributes::decl_attributes(bool is_abbrev, bool persistent): m_is_class = false; m_is_parsing_only = false; m_has_multiple_instances = false; - m_unfold_f_hint = false; + m_unfold_full_hint = false; m_constructor_hint = false; m_symm = false; m_trans = false; @@ -104,19 +104,19 @@ void decl_attributes::parse(buffer const & ns, parser & p) { "marked as '[parsing-only]'", pos); m_is_parsing_only = true; p.next(); - } else if (p.curr_is_token(get_unfold_f_tk())) { + } else if (p.curr_is_token(get_unfold_full_tk())) { p.next(); - m_unfold_f_hint = true; + m_unfold_full_hint = true; } else if (p.curr_is_token(get_constructor_tk())) { p.next(); m_constructor_hint = true; - } else if (p.curr_is_token(get_unfold_c_tk())) { + } else if (p.curr_is_token(get_unfold_tk())) { p.next(); unsigned r = p.parse_small_nat(); if (r == 0) - throw parser_error("invalid '[unfold-c]' attribute, value must be greater than 0", pos); - m_unfold_c_hint = r - 1; - p.check_token_next(get_rbracket_tk(), "invalid 'unfold-c', ']' expected"); + throw parser_error("invalid '[unfold]' attribute, value must be greater than 0", pos); + m_unfold_hint = r - 1; + p.check_token_next(get_rbracket_tk(), "invalid 'unfold', ']' expected"); } else if (p.curr_is_token(get_symm_tk())) { p.next(); m_symm = true; @@ -192,10 +192,10 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c env = set_reducible(env, d, reducible_status::Semireducible, m_persistent); if (m_is_quasireducible) env = set_reducible(env, d, reducible_status::Quasireducible, m_persistent); - if (m_unfold_c_hint) - env = add_unfold_c_hint(env, d, *m_unfold_c_hint, m_persistent); - if (m_unfold_f_hint) - env = add_unfold_f_hint(env, d, m_persistent); + if (m_unfold_hint) + env = add_unfold_hint(env, d, *m_unfold_hint, m_persistent); + if (m_unfold_full_hint) + env = add_unfold_full_hint(env, d, m_persistent); } if (m_constructor_hint) env = add_constructor_hint(env, d, m_persistent); @@ -221,16 +221,16 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c void decl_attributes::write(serializer & s) const { s << m_is_abbrev << m_persistent << m_is_instance << m_is_trans_instance << m_is_coercion << m_is_reducible << m_is_irreducible << m_is_semireducible << m_is_quasireducible - << m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_f_hint + << m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_full_hint << m_constructor_hint << m_symm << m_trans << m_refl << m_subst << m_recursor - << m_rewrite << m_recursor_major_pos << m_priority << m_unfold_c_hint; + << m_rewrite << m_recursor_major_pos << m_priority << m_unfold_hint; } void decl_attributes::read(deserializer & d) { d >> m_is_abbrev >> m_persistent >> m_is_instance >> m_is_trans_instance >> m_is_coercion >> m_is_reducible >> m_is_irreducible >> m_is_semireducible >> m_is_quasireducible - >> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_f_hint + >> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_full_hint >> m_constructor_hint >> m_symm >> m_trans >> m_refl >> m_subst >> m_recursor - >> m_rewrite >> m_recursor_major_pos >> m_priority >> m_unfold_c_hint; + >> m_rewrite >> m_recursor_major_pos >> m_priority >> m_unfold_hint; } } diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h index 621333d30..5473dae89 100644 --- a/src/frontends/lean/decl_attributes.h +++ b/src/frontends/lean/decl_attributes.h @@ -22,7 +22,7 @@ class decl_attributes { bool m_is_class; bool m_is_parsing_only; bool m_has_multiple_instances; - bool m_unfold_f_hint; + bool m_unfold_full_hint; bool m_constructor_hint; bool m_symm; bool m_trans; @@ -32,7 +32,7 @@ class decl_attributes { bool m_rewrite; optional m_recursor_major_pos; optional m_priority; - optional m_unfold_c_hint; + optional m_unfold_hint; void parse(name const & n, parser & p); public: diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 50f5e55f0..0c42c5d7b 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -724,8 +724,8 @@ struct structure_cmd_fn { rec_on_decl.get_type(), rec_on_decl.get_value()); m_env = module::add(m_env, check(m_env, new_decl)); m_env = set_reducible(m_env, n, reducible_status::Reducible); - if (optional idx = has_unfold_c_hint(m_env, rec_on_name)) - m_env = add_unfold_c_hint(m_env, n, *idx); + if (optional idx = has_unfold_hint(m_env, rec_on_name)) + m_env = add_unfold_hint(m_env, n, *idx); save_def_info(n); add_alias(n); } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 846cb92ed..29b512c3b 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -109,8 +109,8 @@ void init_token_table(token_table & t) { "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[trans-instance]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]", "[rewrite]", "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor", - "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-f]", - "[constructor]", "[unfold-c", "print", + "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-full]", "[unfold-hints]", + "[constructor]", "[unfold", "print", "end", "namespace", "section", "prelude", "help", "import", "inductive", "record", "structure", "module", "universe", "universes", "local", "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 7efa4f580..3c603a01c 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -99,8 +99,10 @@ static name const * g_variables_tk = nullptr; static name const * g_instance_tk = nullptr; static name const * g_trans_inst_tk = nullptr; static name const * g_priority_tk = nullptr; -static name const * g_unfold_c_tk = nullptr; -static name const * g_unfold_f_tk = nullptr; +static name const * g_unfold_tk = nullptr; +static name const * g_unfold_full_tk = nullptr; +static name const * g_unfold_hints_bracket_tk = nullptr; +static name const * g_unfold_hints_tk = nullptr; static name const * g_constructor_tk = nullptr; static name const * g_coercion_tk = nullptr; static name const * g_reducible_tk = nullptr; @@ -236,8 +238,10 @@ void initialize_tokens() { g_instance_tk = new name{"[instance]"}; g_trans_inst_tk = new name{"[trans-instance]"}; g_priority_tk = new name{"[priority"}; - g_unfold_c_tk = new name{"[unfold-c"}; - g_unfold_f_tk = new name{"[unfold-f]"}; + g_unfold_tk = new name{"[unfold"}; + g_unfold_full_tk = new name{"[unfold-full]"}; + g_unfold_hints_bracket_tk = new name{"[unfold-hints]"}; + g_unfold_hints_tk = new name{"unfold-hints"}; g_constructor_tk = new name{"[constructor]"}; g_coercion_tk = new name{"[coercion]"}; g_reducible_tk = new name{"[reducible]"}; @@ -374,8 +378,10 @@ void finalize_tokens() { delete g_instance_tk; delete g_trans_inst_tk; delete g_priority_tk; - delete g_unfold_c_tk; - delete g_unfold_f_tk; + delete g_unfold_tk; + delete g_unfold_full_tk; + delete g_unfold_hints_bracket_tk; + delete g_unfold_hints_tk; delete g_constructor_tk; delete g_coercion_tk; delete g_reducible_tk; @@ -511,8 +517,10 @@ name const & get_variables_tk() { return *g_variables_tk; } name const & get_instance_tk() { return *g_instance_tk; } name const & get_trans_inst_tk() { return *g_trans_inst_tk; } name const & get_priority_tk() { return *g_priority_tk; } -name const & get_unfold_c_tk() { return *g_unfold_c_tk; } -name const & get_unfold_f_tk() { return *g_unfold_f_tk; } +name const & get_unfold_tk() { return *g_unfold_tk; } +name const & get_unfold_full_tk() { return *g_unfold_full_tk; } +name const & get_unfold_hints_bracket_tk() { return *g_unfold_hints_bracket_tk; } +name const & get_unfold_hints_tk() { return *g_unfold_hints_tk; } name const & get_constructor_tk() { return *g_constructor_tk; } name const & get_coercion_tk() { return *g_coercion_tk; } name const & get_reducible_tk() { return *g_reducible_tk; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index c0197211b..323195b8e 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -101,8 +101,10 @@ name const & get_variables_tk(); name const & get_instance_tk(); name const & get_trans_inst_tk(); name const & get_priority_tk(); -name const & get_unfold_c_tk(); -name const & get_unfold_f_tk(); +name const & get_unfold_tk(); +name const & get_unfold_full_tk(); +name const & get_unfold_hints_bracket_tk(); +name const & get_unfold_hints_tk(); name const & get_constructor_tk(); name const & get_coercion_tk(); name const & get_reducible_tk(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index 050ceb7ff..a76230e5e 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -94,8 +94,10 @@ variables variables instance [instance] trans_inst [trans-instance] priority [priority -unfold_c [unfold-c -unfold_f [unfold-f] +unfold [unfold +unfold_full [unfold-full] +unfold_hints_bracket [unfold-hints] +unfold_hints unfold-hints constructor [constructor] coercion [coercion] reducible [reducible] diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp index ab3b5de4e..c5683b64f 100644 --- a/src/library/definitional/brec_on.cpp +++ b/src/library/definitional/brec_on.cpp @@ -147,7 +147,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, below_name, reducible_status::Reducible); if (!ibelow) - new_env = add_unfold_c_hint(new_env, below_name, nparams + nindices + ntypeformers); + new_env = add_unfold_hint(new_env, below_name, nparams + nindices + ntypeformers); return add_protected(new_env, below_name); } @@ -333,7 +333,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible); if (!ind) - new_env = add_unfold_c_hint(new_env, brec_on_name, nparams + nindices + ntypeformers); + new_env = add_unfold_hint(new_env, brec_on_name, nparams + nindices + ntypeformers); return add_protected(new_env, brec_on_name); } diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp index e8288b2bc..6fe4628f3 100644 --- a/src/library/definitional/cases_on.cpp +++ b/src/library/definitional/cases_on.cpp @@ -182,7 +182,7 @@ environment mk_cases_on(environment const & env, name const & n) { use_conv_opt); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible); - new_env = add_unfold_c_hint(new_env, cases_on_name, cases_on_major_idx); + new_env = add_unfold_hint(new_env, cases_on_name, cases_on_major_idx); return add_protected(new_env, cases_on_name); } } diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index f1583ae0e..f6aa731b8 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -258,7 +258,7 @@ environment mk_projections(environment const & env, name const & n, buffer use_conv_opt); new_env = module::add(new_env, check(new_env, new_d)); new_env = set_reducible(new_env, proj_name, reducible_status::Reducible); - new_env = add_unfold_c_hint(new_env, proj_name, nparams); + new_env = add_unfold_hint(new_env, proj_name, nparams); new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i, inst_implicit); expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c); intro_type = instantiate(binding_body(intro_type), proj); diff --git a/src/library/definitional/rec_on.cpp b/src/library/definitional/rec_on.cpp index 1925aac4c..6dc7b4210 100644 --- a/src/library/definitional/rec_on.cpp +++ b/src/library/definitional/rec_on.cpp @@ -58,7 +58,7 @@ environment mk_rec_on(environment const & env, name const & n) { check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(), rec_on_type, rec_on_val, use_conv_opt))); new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible); - new_env = add_unfold_c_hint(new_env, rec_on_name, rec_on_major_idx); + new_env = add_unfold_hint(new_env, rec_on_name, rec_on_major_idx); return add_protected(new_env, rec_on_name); } } diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index ce81a34d9..20b9ff412 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -23,35 +23,35 @@ namespace lean { /** \brief unfold hints instruct the normalizer (and simplifier) that a function application. We have two kinds of hints: - - unfold_c (f a_1 ... a_i ... a_n) should be unfolded + - [unfold] (f a_1 ... a_i ... a_n) should be unfolded when argument a_i is a constructor. - - unfold_f (f a_1 ... a_i ... a_n) should be unfolded when it is fully applied. + - [unfold-full] (f a_1 ... a_i ... a_n) should be unfolded when it is fully applied. - constructor (f ...) should be unfolded when it is the major premise of a recursor-like operator */ struct unfold_hint_entry { - enum kind {UnfoldC, UnfoldF, UnfoldM}; + enum kind {Unfold, UnfoldFull, Constructor}; kind m_kind; //!< true if it is an unfold_c hint bool m_add; //!< add/remove hint name m_decl_name; unsigned m_arg_idx; - unfold_hint_entry():m_kind(UnfoldC), m_add(false), m_arg_idx(0) {} + unfold_hint_entry():m_kind(Unfold), m_add(false), m_arg_idx(0) {} unfold_hint_entry(kind k, bool add, name const & n, unsigned idx): m_kind(k), m_add(add), m_decl_name(n), m_arg_idx(idx) {} }; -unfold_hint_entry mk_add_unfold_c_entry(name const & n, unsigned idx) { return unfold_hint_entry(unfold_hint_entry::UnfoldC, true, n, idx); } -unfold_hint_entry mk_erase_unfold_c_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldC, false, n, 0); } -unfold_hint_entry mk_add_unfold_f_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldF, true, n, 0); } -unfold_hint_entry mk_erase_unfold_f_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldF, false, n, 0); } -unfold_hint_entry mk_add_constructor_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldM, true, n, 0); } -unfold_hint_entry mk_erase_constructor_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldM, false, n, 0); } +unfold_hint_entry mk_add_unfold_entry(name const & n, unsigned idx) { return unfold_hint_entry(unfold_hint_entry::Unfold, true, n, idx); } +unfold_hint_entry mk_erase_unfold_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::Unfold, false, n, 0); } +unfold_hint_entry mk_add_unfold_full_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldFull, true, n, 0); } +unfold_hint_entry mk_erase_unfold_full_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldFull, false, n, 0); } +unfold_hint_entry mk_add_constructor_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::Constructor, true, n, 0); } +unfold_hint_entry mk_erase_constructor_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::Constructor, false, n, 0); } static name * g_unfold_hint_name = nullptr; static std::string * g_key = nullptr; struct unfold_hint_state { - name_map m_unfold_c; - name_set m_unfold_f; + name_map m_unfold; + name_set m_unfold_full; name_set m_constructor; }; @@ -61,19 +61,19 @@ struct unfold_hint_config { static void add_entry(environment const &, io_state const &, state & s, entry const & e) { switch (e.m_kind) { - case unfold_hint_entry::UnfoldC: + case unfold_hint_entry::Unfold: if (e.m_add) - s.m_unfold_c.insert(e.m_decl_name, e.m_arg_idx); + s.m_unfold.insert(e.m_decl_name, e.m_arg_idx); else - s.m_unfold_c.erase(e.m_decl_name); + s.m_unfold.erase(e.m_decl_name); break; - case unfold_hint_entry::UnfoldF: + case unfold_hint_entry::UnfoldFull: if (e.m_add) - s.m_unfold_f.insert(e.m_decl_name); + s.m_unfold_full.insert(e.m_decl_name); else - s.m_unfold_f.erase(e.m_decl_name); + s.m_unfold_full.erase(e.m_decl_name); break; - case unfold_hint_entry::UnfoldM: + case unfold_hint_entry::Constructor: if (e.m_add) s.m_constructor.insert(e.m_decl_name); else @@ -105,39 +105,39 @@ struct unfold_hint_config { template class scoped_ext; typedef scoped_ext unfold_hint_ext; -environment add_unfold_c_hint(environment const & env, name const & n, unsigned idx, bool persistent) { +environment add_unfold_hint(environment const & env, name const & n, unsigned idx, bool persistent) { declaration const & d = env.get(n); if (!d.is_definition()) - throw exception("invalid unfold-c hint, declaration must be a non-opaque definition"); - return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_c_entry(n, idx), persistent); + throw exception("invalid [unfold] hint, declaration must be a non-opaque definition"); + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_entry(n, idx), persistent); } -optional has_unfold_c_hint(environment const & env, name const & d) { +optional has_unfold_hint(environment const & env, name const & d) { unfold_hint_state const & s = unfold_hint_ext::get_state(env); - if (auto it = s.m_unfold_c.find(d)) + if (auto it = s.m_unfold.find(d)) return optional(*it); else return optional(); } -environment erase_unfold_c_hint(environment const & env, name const & n, bool persistent) { - return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_c_entry(n), persistent); +environment erase_unfold_hint(environment const & env, name const & n, bool persistent) { + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_entry(n), persistent); } -environment add_unfold_f_hint(environment const & env, name const & n, bool persistent) { +environment add_unfold_full_hint(environment const & env, name const & n, bool persistent) { declaration const & d = env.get(n); if (!d.is_definition()) - throw exception("invalid unfold-f hint, declaration must be a non-opaque definition"); - return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_f_entry(n), persistent); + throw exception("invalid [unfold-full] hint, declaration must be a non-opaque definition"); + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_full_entry(n), persistent); } -bool has_unfold_f_hint(environment const & env, name const & d) { +bool has_unfold_full_hint(environment const & env, name const & d) { unfold_hint_state const & s = unfold_hint_ext::get_state(env); - return s.m_unfold_f.contains(d); + return s.m_unfold_full.contains(d); } -environment erase_unfold_f_hint(environment const & env, name const & n, bool persistent) { - return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_f_entry(n), persistent); +environment erase_unfold_full_hint(environment const & env, name const & n, bool persistent) { + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_full_entry(n), persistent); } environment add_constructor_hint(environment const & env, name const & n, bool persistent) { @@ -246,14 +246,14 @@ class normalize_fn { return update_binding(e, d, b); } - optional has_unfold_c_hint(expr const & f) { + optional has_unfold_hint(expr const & f) { if (!is_constant(f)) return optional(); - return ::lean::has_unfold_c_hint(env(), const_name(f)); + return ::lean::has_unfold_hint(env(), const_name(f)); } - bool has_unfold_f_hint(expr const & f) { - return is_constant(f) && ::lean::has_unfold_f_hint(env(), const_name(f)); + bool has_unfold_full_hint(expr const & f) { + return is_constant(f) && ::lean::has_unfold_full_hint(env(), const_name(f)); } optional is_constructor_like(expr const & e) { @@ -305,13 +305,13 @@ class normalize_fn { modified = true; a = new_a; } - if (has_unfold_f_hint(f)) { + if (has_unfold_full_hint(f)) { if (!is_pi(m_tc.whnf(m_tc.infer(e).first).first)) { if (optional r = unfold_app(env(), mk_rev_app(f, args))) return normalize(*r); } } - if (auto idx = has_unfold_c_hint(f)) { + if (auto idx = has_unfold_hint(f)) { if (auto r = unfold_recursor_like(f, *idx, args)) return *r; } diff --git a/src/library/normalize.h b/src/library/normalize.h index 217bde2c5..4cc331c71 100644 --- a/src/library/normalize.h +++ b/src/library/normalize.h @@ -32,7 +32,7 @@ expr normalize(type_checker & tc, expr const & e, constraint_seq & cs, bool eta expr normalize(type_checker & tc, expr const & e, std::function const & pred, // NOLINT constraint_seq & cs, bool eta = false); -/** \brief unfold-c hint instructs the normalizer (and simplifier) that +/** \brief [unfold] hint instructs the normalizer (and simplifier) that a function application (f a_1 ... a_i ... a_n) should be unfolded when argument a_i is a constructor. @@ -40,17 +40,17 @@ expr normalize(type_checker & tc, expr const & e, std::function has_unfold_c_hint(environment const & env, name const & d); +environment add_unfold_hint(environment const & env, name const & n, unsigned idx, bool persistent = true); +environment erase_unfold_hint(environment const & env, name const & n, bool persistent = true); +/** \brief Retrieve the hint added with the procedure add_unfold_hint. */ +optional has_unfold_hint(environment const & env, name const & d); -/** \brief unfold-f hint instructs normalizer (and simplifier) that function application +/** \brief [unfold-full] hint instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied */ -environment add_unfold_f_hint(environment const & env, name const & n, bool persistent = true); -environment erase_unfold_f_hint(environment const & env, name const & n, bool persistent = true); -/** \brief Retrieve the hint added with the procedure add_unfold_f_hint. */ -optional has_unfold_f_hint(environment const & env, name const & d); +environment add_unfold_full_hint(environment const & env, name const & n, bool persistent = true); +environment erase_unfold_full_hint(environment const & env, name const & n, bool persistent = true); +/** \brief Retrieve the hint added with the procedure add_unfold_full_hint. */ +optional has_unfold_full_hint(environment const & env, name const & d); /** \brief unfold-m hint instructs normalizer (and simplifier) that function application diff --git a/tests/lean/640.hlean b/tests/lean/640.hlean index b70593930..29f59ef48 100644 --- a/tests/lean/640.hlean +++ b/tests/lean/640.hlean @@ -6,7 +6,7 @@ open quotient eq sum local abbreviation C := quotient R - definition f [unfold-c 2] (a : A) (x : unit) : C := + definition f [unfold 2] (a : A) (x : unit) : C := !class_of a inductive S : C → C → Type := diff --git a/tests/lean/run/all_goals.lean b/tests/lean/run/all_goals.lean index af985d809..28408aaf7 100644 --- a/tests/lean/run/all_goals.lean +++ b/tests/lean/run/all_goals.lean @@ -1,8 +1,8 @@ import data.nat open nat -attribute nat.add [unfold-c 2] -attribute nat.rec_on [unfold-c 2] +attribute nat.add [unfold 2] +attribute nat.rec_on [unfold 2] example (a b c : nat) : a + 0 = 0 + a ∧ b + 0 = 0 + b := begin diff --git a/tests/lean/run/all_goals2.lean b/tests/lean/run/all_goals2.lean index 3a5aec2c4..d7e7e0f9d 100644 --- a/tests/lean/run/all_goals2.lean +++ b/tests/lean/run/all_goals2.lean @@ -1,8 +1,8 @@ import data.nat open nat -attribute nat.add [unfold-c 2] -attribute nat.rec_on [unfold-c 2] +attribute nat.add [unfold 2] +attribute nat.rec_on [unfold 2] infixl `;`:15 := tactic.and_then diff --git a/tests/lean/run/rewriter14.lean b/tests/lean/run/rewriter14.lean index 3883ddba5..4672933c4 100644 --- a/tests/lean/run/rewriter14.lean +++ b/tests/lean/run/rewriter14.lean @@ -1,10 +1,10 @@ import data.nat open nat -definition f [unfold-c 2] (x y z : nat) : nat := +definition f [unfold 2] (x y z : nat) : nat := x + y + z -attribute of_num [unfold-c 1] +attribute of_num [unfold 1] example (x y : nat) (H1 : f x 0 0 = 0) : x = 0 := begin diff --git a/tests/lean/unfoldf.lean b/tests/lean/unfoldf.lean index 8deb1c48c..95bd708db 100644 --- a/tests/lean/unfoldf.lean +++ b/tests/lean/unfoldf.lean @@ -1,6 +1,6 @@ open nat -definition id [unfold-f] {A : Type} (a : A) := a +definition id [unfold-full] {A : Type} (a : A) := a definition compose {A B C : Type} (g : B → C) (f : A → B) (a : A) := g (f a) notation g ∘ f := compose g f @@ -18,7 +18,7 @@ begin exact H end -attribute compose [unfold-f] +attribute compose [unfold-full] example (a b : nat) (H : a = b) : (id ∘ id) a = b := begin