From b4d6f6e3edd746f2bdddbc6586c29ec5fd312ec7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Jan 2015 11:31:12 -0800 Subject: [PATCH] feat(frontends/lean): 'attribute' command is persistent by default --- doc/lean/reducible.org | 15 +++--- hott/algebra/category/basic.hlean | 4 +- hott/algebra/category/set.hlean | 2 +- hott/algebra/group.hlean | 48 ++++++++++---------- hott/algebra/groupoid.hlean | 2 +- hott/algebra/precategory/basic.hlean | 4 +- hott/algebra/precategory/constructions.hlean | 4 +- hott/algebra/precategory/functor.hlean | 6 +-- hott/algebra/precategory/morphism.hlean | 4 +- hott/init/axioms/funext_varieties.hlean | 2 +- hott/init/equiv.hlean | 2 +- hott/init/hedberg.hlean | 2 +- hott/init/nat.hlean | 2 +- hott/init/trunc.hlean | 2 +- hott/types/sigma.hlean | 2 +- library/algebra/category/basic.lean | 2 +- library/algebra/category/constructions.lean | 14 +++--- library/algebra/category/functor.lean | 10 ++-- library/algebra/category/morphism.lean | 4 +- library/algebra/group.lean | 48 ++++++++++---------- library/data/bool.lean | 4 +- library/data/int/basic.lean | 2 +- library/data/list/basic.lean | 4 +- library/data/nat/div.lean | 2 +- library/init/nat.lean | 2 +- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_cmds.cpp | 10 ++++ src/frontends/lean/decl_cmds.cpp | 8 ++-- src/frontends/lean/decl_cmds.h | 6 ++- src/frontends/lean/notation_cmd.cpp | 5 ++ src/frontends/lean/notation_cmd.h | 3 ++ src/frontends/lean/token_table.cpp | 4 +- tests/lean/run/e6.lean | 2 +- tests/lean/run/e9.lean | 2 +- tests/lean/run/fibrant_class1.lean | 2 +- tests/lean/run/fibrant_class2.lean | 2 +- tests/lean/run/group4.lean | 16 +++---- tests/lean/run/group5.lean | 16 +++---- 38 files changed, 145 insertions(+), 126 deletions(-) diff --git a/doc/lean/reducible.org b/doc/lean/reducible.org index 428471720..fd0cce77a 100644 --- a/doc/lean/reducible.org +++ b/doc/lean/reducible.org @@ -59,9 +59,9 @@ definition pr1 [reducible] (A : Type) (a b : A) : A := a #+END_SRC The =reducible= attribute is saved in the compiled .olean files. The user -can temporarily change the =reducible= and =irreducible= attributes using -the =attribute= command. The temporary modification is effective only in the -current file, and is not saved in the produced .olean file. +can change the =reducible= and =irreducible= attributes using +the =attribute= command. The modification is saved in the +produced .olean file. #+BEGIN_SRC lean definition id (A : Type) (a : A) : A := a @@ -74,12 +74,13 @@ current file, and is not saved in the produced .olean file. attribute pr2 [irreducible] #+END_SRC -The command =persistent attribute= can be used to instruct Lean to make the -modification permanent, and save it in the .olean file. +The command =local attribute= can be used to instruct Lean to not save +the new attribute in the .olean file. If the =attibute= command is used +inside of a =context=, then the scope of its effect is the current scope. #+BEGIN_SRC lean definition pr2 (A : Type) (a b : A) : A := b -- Mark pr2 as irreducible. - -- The modification will affect modules that import this one. - persistent attribute pr2 [irreducible] + -- The modification will not affect modules that import this one. + local attribute pr2 [irreducible] #+END_SRC diff --git a/hott/algebra/category/basic.hlean b/hott/algebra/category/basic.hlean index 7c991a26d..15883de25 100644 --- a/hott/algebra/category/basic.hlean +++ b/hott/algebra/category/basic.hlean @@ -12,7 +12,7 @@ open precategory morphism is_equiv eq truncation nat sigma sigma.ops structure category [class] (ob : Type) extends (precategory ob) := (iso_of_path_equiv : Π {a b : ob}, is_equiv (@iso_of_path ob (precategory.mk hom _ comp ID assoc id_left id_right) a b)) -persistent attribute category [multiple-instances] +attribute category [multiple-instances] namespace category variables {ob : Type} {C : category ob} {a b : ob} @@ -20,7 +20,7 @@ namespace category -- Make iso_of_path_equiv a class instance -- TODO: Unsafe class instance? - persistent attribute iso_of_path_equiv [instance] + attribute iso_of_path_equiv [instance] definition path_of_iso {a b : ob} : a ≅ b → a = b := iso_of_path⁻¹ diff --git a/hott/algebra/category/set.hlean b/hott/algebra/category/set.hlean index 63fbe4b97..761cd67d7 100644 --- a/hott/algebra/category/set.hlean +++ b/hott/algebra/category/set.hlean @@ -29,7 +29,7 @@ end precategory namespace category universe variable l - attribute precategory.set_precategory.{l+1 l} [instance] + local attribute precategory.set_precategory.{l+1 l} [instance] definition set_category_equiv_iso (a b : (Σ (A : Type.{l}), is_hset A)) : (a ≅ b) = (a.1 ≃ b.1) := diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean index b5a869c55..fc97286f5 100644 --- a/hott/algebra/group.hlean +++ b/hott/algebra/group.hlean @@ -493,73 +493,73 @@ end add_comm_group structure Semigroup := (carrier : Type) (struct : semigroup carrier) -persistent attribute Semigroup.carrier [coercion] -persistent attribute Semigroup.struct [instance] +attribute Semigroup.carrier [coercion] +attribute Semigroup.struct [instance] structure CommSemigroup := (carrier : Type) (struct : comm_semigroup carrier) -persistent attribute CommSemigroup.carrier [coercion] -persistent attribute CommSemigroup.struct [instance] +attribute CommSemigroup.carrier [coercion] +attribute CommSemigroup.struct [instance] structure Monoid := (carrier : Type) (struct : monoid carrier) -persistent attribute Monoid.carrier [coercion] -persistent attribute Monoid.struct [instance] +attribute Monoid.carrier [coercion] +attribute Monoid.struct [instance] structure CommMonoid := (carrier : Type) (struct : comm_monoid carrier) -persistent attribute CommMonoid.carrier [coercion] -persistent attribute CommMonoid.struct [instance] +attribute CommMonoid.carrier [coercion] +attribute CommMonoid.struct [instance] structure Group := (carrier : Type) (struct : group carrier) -persistent attribute Group.carrier [coercion] -persistent attribute Group.struct [instance] +attribute Group.carrier [coercion] +attribute Group.struct [instance] structure CommGroup := (carrier : Type) (struct : comm_group carrier) -persistent attribute CommGroup.carrier [coercion] -persistent attribute CommGroup.struct [instance] +attribute CommGroup.carrier [coercion] +attribute CommGroup.struct [instance] structure AddSemigroup := (carrier : Type) (struct : add_semigroup carrier) -persistent attribute AddSemigroup.carrier [coercion] -persistent attribute AddSemigroup.struct [instance] +attribute AddSemigroup.carrier [coercion] +attribute AddSemigroup.struct [instance] structure AddCommSemigroup := (carrier : Type) (struct : add_comm_semigroup carrier) -persistent attribute AddCommSemigroup.carrier [coercion] -persistent attribute AddCommSemigroup.struct [instance] +attribute AddCommSemigroup.carrier [coercion] +attribute AddCommSemigroup.struct [instance] structure AddMonoid := (carrier : Type) (struct : add_monoid carrier) -persistent attribute AddMonoid.carrier [coercion] -persistent attribute AddMonoid.struct [instance] +attribute AddMonoid.carrier [coercion] +attribute AddMonoid.struct [instance] structure AddCommMonoid := (carrier : Type) (struct : add_comm_monoid carrier) -persistent attribute AddCommMonoid.carrier [coercion] -persistent attribute AddCommMonoid.struct [instance] +attribute AddCommMonoid.carrier [coercion] +attribute AddCommMonoid.struct [instance] structure AddGroup := (carrier : Type) (struct : add_group carrier) -persistent attribute AddGroup.carrier [coercion] -persistent attribute AddGroup.struct [instance] +attribute AddGroup.carrier [coercion] +attribute AddGroup.struct [instance] structure AddCommGroup := (carrier : Type) (struct : add_comm_group carrier) -persistent attribute AddCommGroup.carrier [coercion] -persistent attribute AddCommGroup.struct [instance] +attribute AddCommGroup.carrier [coercion] +attribute AddCommGroup.struct [instance] end path_algebra diff --git a/hott/algebra/groupoid.hlean b/hott/algebra/groupoid.hlean index a9f6270da..ab7e0ef0e 100644 --- a/hott/algebra/groupoid.hlean +++ b/hott/algebra/groupoid.hlean @@ -14,7 +14,7 @@ structure groupoid [class] (ob : Type) extends precategory ob := namespace groupoid -persistent attribute all_iso [instance] +attribute all_iso [instance] --set_option pp.universes true --set_option pp.implicit true diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean index 252769153..2b9ba9e83 100644 --- a/hott/algebra/precategory/basic.hlean +++ b/hott/algebra/precategory/basic.hlean @@ -14,13 +14,13 @@ structure precategory [class] (ob : Type) : Type := (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f) (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f) -persistent attribute precategory [multiple-instances] +attribute precategory [multiple-instances] namespace precategory variables {ob : Type} [C : precategory ob] variables {a b c d : ob} include C - persistent attribute homH [instance] + attribute homH [instance] definition compose := comp diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean index 8d915e95a..c3ce6dcee 100644 --- a/hott/algebra/precategory/constructions.hlean +++ b/hott/algebra/precategory/constructions.hlean @@ -110,7 +110,7 @@ namespace precategory infixr `×c`:30 := product.Prod_precategory --instance [persistent] type_category category_one -- category_two product.prod_category - persistent attribute product.prod_precategory [instance] + attribute product.prod_precategory [instance] end ops @@ -218,7 +218,7 @@ namespace precategory exit definition Slice_category [reducible] (C : Category) (c : C) := Mk (slice_category C c) open category.ops - instance [persistent] slice_category + attribute slice_category [instance] variables {D : Category} definition forgetful (x : D) : (Slice_category D x) ⇒ D := functor.mk (λ a, to_ob a) diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean index 5b1fc5b3c..1617b901f 100644 --- a/hott/algebra/precategory/functor.hlean +++ b/hott/algebra/precategory/functor.hlean @@ -19,8 +19,8 @@ infixl `⇒`:25 := functor namespace functor variables {C D E : Precategory} - persistent attribute obF [coercion] - persistent attribute homF [coercion] + attribute obF [coercion] + attribute homF [coercion] -- "functor C D" is equivalent to a certain sigma type set_option unifier.max_steps 38500 @@ -156,7 +156,7 @@ namespace precategory namespace ops notation `PreCat`:max := Precat_of_strict_cats - persistent attribute precat_of_strict_precats [instance] + attribute precat_of_strict_precats [instance] end ops diff --git a/hott/algebra/precategory/morphism.hlean b/hott/algebra/precategory/morphism.hlean index 3e21c1074..ed8d5ec03 100644 --- a/hott/algebra/precategory/morphism.hlean +++ b/hott/algebra/precategory/morphism.hlean @@ -16,7 +16,7 @@ namespace morphism inductive is_iso [class] (f : a ⟶ b) : Type := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f - persistent attribute is_iso [multiple-instances] + attribute is_iso [multiple-instances] definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a := is_section.rec (λg h, g) H @@ -133,7 +133,7 @@ namespace morphism namespace isomorphic -- openrelation - persistent attribute is_iso [instance] + attribute is_iso [instance] definition refl (a : ob) : a ≅ a := mk id diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean index b3d5b4ff8..e4b29b466 100644 --- a/hott/init/axioms/funext_varieties.hlean +++ b/hott/init/axioms/funext_varieties.hlean @@ -85,7 +85,7 @@ context @transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f idhtpy) (sigma.mk g h) (@path_contr _ contr_basedhtpy _ _) d - attribute htpy_ind [reducible] + local attribute htpy_ind [reducible] definition htpy_ind_beta : htpy_ind f idhtpy = d := (@path2_contr _ _ _ _ !path_contr idp)⁻¹ ▹ idp diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 048a2d09c..ba11648af 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -212,7 +212,7 @@ end is_equiv namespace equiv - persistent attribute to_is_equiv [instance] + attribute to_is_equiv [instance] infix `≃`:25 := equiv diff --git a/hott/init/hedberg.hlean b/hott/init/hedberg.hlean index aaff2c60e..ce9c2799b 100644 --- a/hott/init/hedberg.hlean +++ b/hott/init/hedberg.hlean @@ -43,4 +43,4 @@ context ... = q : aux) end -persistent attribute is_hset_of_decidable_eq [instance] +attribute is_hset_of_decidable_eq [instance] diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index 7fd2a6d89..c85aae01d 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -296,7 +296,7 @@ namespace nat notation a * b := mul a b - attribute sub [reducible] + local attribute sub [reducible] definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b := rec_on b rfl diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index c6ef3f9ea..d8ed45571 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -188,7 +188,7 @@ namespace truncation structure trunctype (n : trunc_index) := (trunctype_type : Type) (is_trunc_trunctype_type : is_trunc n trunctype_type) - attribute trunctype.trunctype_type [coercion] + local attribute trunctype.trunctype_type [coercion] notation n `-Type` := trunctype n notation `hprop` := -1-Type diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index ddc02fce6..d1f462d6e 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -142,7 +142,7 @@ namespace sigma apply dpair_eq_dpair_pp_pp end - attribute dpair_eq_dpair [reducible] + local attribute dpair_eq_dpair [reducible] definition dpair_eq_dpair_p1_1p (p : a = a') (q : p ▹ b = b') : dpair_eq_dpair p q = dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q := begin diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean index 17ea1e45d..f8dee3ef6 100644 --- a/library/algebra/category/basic.lean +++ b/library/algebra/category/basic.lean @@ -19,7 +19,7 @@ structure category [class] (ob : Type) : Type := (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f) (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f) -persistent attribute category [multiple-instances] +attribute category [multiple-instances] namespace category variables {ob : Type} [C : category ob] diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean index 88b007ff5..81a0bdfc8 100644 --- a/library/algebra/category/constructions.lean +++ b/library/algebra/category/constructions.lean @@ -77,10 +77,10 @@ namespace category (λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _) (λ a b f, @subsingleton.elim (set_hom a b) _ _ _) (λ a b f, @subsingleton.elim (set_hom a b) _ _ _) - attribute discrete_category [reducible] + local attribute discrete_category [reducible] definition Discrete_category (A : Type) [H : decidable_eq A] := Mk (discrete_category A) context - attribute discrete_category [instance] + local attribute discrete_category [instance] include H theorem dicrete_category.endomorphism {a b : A} (f : a ⟶ b) : a = b := decidable.rec_on (H a b) (λh f, h) (λh f, empty.rec _ f) f @@ -125,10 +125,10 @@ namespace category notation 2 := Category_two postfix `ᵒᵖ`:max := opposite.Opposite infixr `×c`:30 := product.Prod_category - persistent attribute type_category [instance] - persistent attribute category_one [instance] - persistent attribute category_two [instance] - persistent attribute product.prod_category [instance] + attribute type_category [instance] + attribute category_one [instance] + attribute category_two [instance] + attribute product.prod_category [instance] end ops open ops @@ -228,7 +228,7 @@ namespace category definition Slice_category [reducible] (C : Category) (c : C) := Mk (slice_category C c) open category.ops - persistent attribute slice_category [instance] + attribute slice_category [instance] variables {D : Category} definition forgetful (x : D) : (Slice_category D x) ⇒ D := functor.mk (λ a, to_ob a) diff --git a/library/algebra/category/functor.lean b/library/algebra/category/functor.lean index 0feb78a61..10f29442d 100644 --- a/library/algebra/category/functor.lean +++ b/library/algebra/category/functor.lean @@ -21,10 +21,10 @@ structure functor (C D : Category) : Type := infixl `⇒`:25 := functor namespace functor - persistent attribute object [coercion] - persistent attribute morphism [coercion] - persistent attribute respect_id [irreducible] - persistent attribute respect_comp [irreducible] + attribute object [coercion] + attribute morphism [coercion] + attribute respect_id [irreducible] + attribute respect_comp [irreducible] variables {A B C D : Category} @@ -71,7 +71,7 @@ namespace category namespace ops notation `Cat`:max := Category_of_categories - persistent attribute category_of_categories [instance] + attribute category_of_categories [instance] end ops end category diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean index f90cc4be0..dfa3ab595 100644 --- a/library/algebra/category/morphism.lean +++ b/library/algebra/category/morphism.lean @@ -20,7 +20,7 @@ namespace morphism inductive is_iso [class] (f : a ⟶ b) : Type := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f - persistent attribute is_iso [multiple-instances] + attribute is_iso [multiple-instances] definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a := is_section.rec (λg h, g) H @@ -131,7 +131,7 @@ namespace morphism namespace isomorphic open relation - persistent attribute is_iso [instance] + attribute is_iso [instance] theorem refl (a : ob) : a ≅ a := mk id theorem symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := mk (inverse (iso H)) diff --git a/library/algebra/group.lean b/library/algebra/group.lean index c47998962..d9fd0cff0 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -489,73 +489,73 @@ end add_comm_group structure Semigroup := (carrier : Type) (struct : semigroup carrier) -persistent attribute Semigroup.carrier [coercion] -persistent attribute Semigroup.struct [instance] +attribute Semigroup.carrier [coercion] +attribute Semigroup.struct [instance] structure CommSemigroup := (carrier : Type) (struct : comm_semigroup carrier) -persistent attribute CommSemigroup.carrier [coercion] -persistent attribute CommSemigroup.struct [instance] +attribute CommSemigroup.carrier [coercion] +attribute CommSemigroup.struct [instance] structure Monoid := (carrier : Type) (struct : monoid carrier) -persistent attribute Monoid.carrier [coercion] -persistent attribute Monoid.struct [instance] +attribute Monoid.carrier [coercion] +attribute Monoid.struct [instance] structure CommMonoid := (carrier : Type) (struct : comm_monoid carrier) -persistent attribute CommMonoid.carrier [coercion] -persistent attribute CommMonoid.struct [instance] +attribute CommMonoid.carrier [coercion] +attribute CommMonoid.struct [instance] structure Group := (carrier : Type) (struct : group carrier) -persistent attribute Group.carrier [coercion] -persistent attribute Group.struct [instance] +attribute Group.carrier [coercion] +attribute Group.struct [instance] structure CommGroup := (carrier : Type) (struct : comm_group carrier) -persistent attribute CommGroup.carrier [coercion] -persistent attribute CommGroup.struct [instance] +attribute CommGroup.carrier [coercion] +attribute CommGroup.struct [instance] structure AddSemigroup := (carrier : Type) (struct : add_semigroup carrier) -persistent attribute AddSemigroup.carrier [coercion] -persistent attribute AddSemigroup.struct [instance] +attribute AddSemigroup.carrier [coercion] +attribute AddSemigroup.struct [instance] structure AddCommSemigroup := (carrier : Type) (struct : add_comm_semigroup carrier) -persistent attribute AddCommSemigroup.carrier [coercion] -persistent attribute AddCommSemigroup.struct [instance] +attribute AddCommSemigroup.carrier [coercion] +attribute AddCommSemigroup.struct [instance] structure AddMonoid := (carrier : Type) (struct : add_monoid carrier) -persistent attribute AddMonoid.carrier [coercion] -persistent attribute AddMonoid.struct [instance] +attribute AddMonoid.carrier [coercion] +attribute AddMonoid.struct [instance] structure AddCommMonoid := (carrier : Type) (struct : add_comm_monoid carrier) -persistent attribute AddCommMonoid.carrier [coercion] -persistent attribute AddCommMonoid.struct [instance] +attribute AddCommMonoid.carrier [coercion] +attribute AddCommMonoid.struct [instance] structure AddGroup := (carrier : Type) (struct : add_group carrier) -persistent attribute AddGroup.carrier [coercion] -persistent attribute AddGroup.struct [instance] +attribute AddGroup.carrier [coercion] +attribute AddGroup.struct [instance] structure AddCommGroup := (carrier : Type) (struct : add_comm_group carrier) -persistent attribute AddCommGroup.carrier [coercion] -persistent attribute AddCommGroup.struct [instance] +attribute AddCommGroup.carrier [coercion] +attribute AddCommGroup.struct [instance] end algebra diff --git a/library/data/bool.lean b/library/data/bool.lean index 36f1b16e7..452c578f6 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -10,8 +10,8 @@ import logic.eq open eq eq.ops decidable namespace bool - attribute bor [reducible] - attribute band [reducible] + local attribute bor [reducible] + local attribute band [reducible] theorem dichotomy (b : bool) : b = ff ∨ b = tt := cases_on b (or.inl rfl) (or.inr rfl) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 1a88a63aa..b2590cb29 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -42,7 +42,7 @@ inductive int : Type := neg_succ_of_nat : nat → int notation `ℤ` := int -persistent attribute int.of_nat [coercion] +attribute int.of_nat [coercion] definition int.of_num [coercion] [reducible] (n : num) : ℤ := int.of_nat (nat.of_num n) namespace int diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 3723e74cc..7d30a58a5 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -197,8 +197,8 @@ induction_on s theorem mem_concat (x : T) (s t : list T) : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t := iff.intro mem_concat_imp_or mem_or_imp_concat -attribute mem [reducible] -attribute append [reducible] +local attribute mem [reducible] +local attribute append [reducible] theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) := induction_on l (take H : x ∈ nil, false.elim (iff.elim_left !mem_nil H)) diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 8f8d88be0..fc9a08668 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -333,7 +333,7 @@ private definition pair_nat.lt : nat × nat → nat × nat → Prop := measure p private definition pair_nat.lt.wf : well_founded pair_nat.lt := intro_k (measure.wf pr₂) 20 -- we use intro_k to be able to execute gcd efficiently in the kernel -attribute pair_nat.lt.wf [instance] -- instance will not be saved in .olean +local attribute pair_nat.lt.wf [instance] -- instance will not be saved in .olean infixl [local] `≺`:50 := pair_nat.lt private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) := diff --git a/library/init/nat.lean b/library/init/nat.lean index 683f3353f..2a317b433 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -288,7 +288,7 @@ namespace nat notation a * b := mul a b - section + context attribute sub [reducible] definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b := induction_on b diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index da62b89f2..73e303716 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -16,7 +16,7 @@ "calc_trans" "calc_subst" "calc_refl" "calc_symm" "match" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "section" "fields" "find_decl" - "attribute" "persistent" "set_option" "add_rewrite" "extends" "include" "omit" "classes" + "attribute" "local" "set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "raw") "lean keywords") diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 9e5ae69ee..8f1e50222 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -575,6 +575,15 @@ environment telescope_eq_cmd(parser & p) { return p.env(); } +environment local_cmd(parser & p) { + if (p.curr_is_token_or_id(get_attribute_tk())) { + p.next(); + return local_attribute_cmd(p); + } else { + return local_notation_cmd(p); + } +} + void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("open", "create aliases for declarations, and use objects defined in other namespaces", open_cmd)); @@ -590,6 +599,7 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd)); add_cmd(r, cmd_info("eval", "evaluate given expression", eval_cmd)); add_cmd(r, cmd_info("find_decl", "find definitions and/or theorems", find_cmd)); + add_cmd(r, cmd_info("local", "define local attributes or notation", local_cmd)); add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd)); add_cmd(r, cmd_info("#projections", "generate projections for inductive datatype (for debugging purposes)", projections_cmd)); add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd)); diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 40722e6a4..067b255ac 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -1015,12 +1015,11 @@ static environment attribute_cmd_core(parser & p, bool persistent) { } static environment attribute_cmd(parser & p) { - return attribute_cmd_core(p, false); + return attribute_cmd_core(p, true); } -static environment persistent_attribute_cmd(parser & p) { - p.check_token_next(get_attribute_tk(), "invalid command, 'attribute' expected"); - return attribute_cmd_core(p, true); +environment local_attribute_cmd(parser & p) { + return attribute_cmd_core(p, false); } void register_decl_cmds(cmd_table & r) { @@ -1041,7 +1040,6 @@ void register_decl_cmds(cmd_table & r) { add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd)); add_cmd(r, cmd_info("include", "force section parameter/variable to be included", include_cmd)); add_cmd(r, cmd_info("attribute", "set declaration attributes", attribute_cmd)); - add_cmd(r, cmd_info("persistent", "set declaration attributes (the value is saved in .olean files)", persistent_attribute_cmd)); add_cmd(r, cmd_info("omit", "undo 'include' command", omit_cmd)); } } diff --git a/src/frontends/lean/decl_cmds.h b/src/frontends/lean/decl_cmds.h index c66a7bd4b..510e1dc4f 100644 --- a/src/frontends/lean/decl_cmds.h +++ b/src/frontends/lean/decl_cmds.h @@ -17,10 +17,12 @@ class parser; */ bool parse_univ_params(parser & p, buffer & ps); expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos); -/** - \brief Add universe levels from \c found_ls to \c ls_buffer (only the levels that do not already occur in \c ls_buffer are added). +/** \brief Add universe levels from \c found_ls to \c ls_buffer (only the levels that do not already occur in \c ls_buffer are added). Then sort \c ls_buffer (using the order in which the universe levels were declared). */ void update_univ_parameters(buffer & ls_buffer, name_set const & found_ls, parser const & p); + +/** \brief Parse a local attribute command */ +environment local_attribute_cmd(parser & p); void register_decl_cmds(cmd_table & r); } diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 51df81474..35cc9d222 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -685,6 +685,11 @@ static environment prefix_cmd(parser & p) { return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve); } +environment local_notation_cmd(parser & p) { + // TODO(Leo) + return p.env(); +} + static environment reserve_cmd(parser & p) { bool overload = false; bool reserve = true; diff --git a/src/frontends/lean/notation_cmd.h b/src/frontends/lean/notation_cmd.h index a0d31bfc1..7e5d28228 100644 --- a/src/frontends/lean/notation_cmd.h +++ b/src/frontends/lean/notation_cmd.h @@ -17,5 +17,8 @@ bool curr_is_notation_decl(parser & p); */ notation_entry parse_notation(parser & p, bool overload, buffer & new_tokens, bool allow_local); +/** \brief Parse local notation */ +environment local_notation_cmd(parser & p); + void register_notation_cmds(cmd_table & r); } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 6a3b7127b..04ce298f6 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -84,14 +84,14 @@ void init_token_table(token_table & t) { {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0}, - {"