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

feat(frontends/lean): 'attribute' command is persistent by default

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-26 11:31:12 -08:00
parent a1eeb0a6a1
commit b4d6f6e3ed
38 changed files with 145 additions and 126 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
doc/lean/reducible.org
View file

@ -59,9 +59,9 @@ definition pr1 [reducible] (A : Type) (a b : A) : A := a
#+END_SRC #+END_SRC
The =reducible= attribute is saved in the compiled .olean files. The user The =reducible= attribute is saved in the compiled .olean files. The user
can temporarily change the =reducible= and =irreducible= attributes using can change the =reducible= and =irreducible= attributes using
the =attribute= command. The temporary modification is effective only in the the =attribute= command. The modification is saved in the
current file, and is not saved in the produced .olean file. produced .olean file.
#+BEGIN_SRC lean #+BEGIN_SRC lean
definition id (A : Type) (a : A) : A := a 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] attribute pr2 [irreducible]
#+END_SRC #+END_SRC
The command =persistent attribute= can be used to instruct Lean to make the The command =local attribute= can be used to instruct Lean to not save
modification permanent, and save it in the .olean file. 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 #+BEGIN_SRC lean
definition pr2 (A : Type) (a b : A) : A := b definition pr2 (A : Type) (a b : A) : A := b
-- Mark pr2 as irreducible. -- Mark pr2 as irreducible.
-- The modification will affect modules that import this one. -- The modification will not affect modules that import this one.
persistent attribute pr2 [irreducible] local attribute pr2 [irreducible]
#+END_SRC #+END_SRC

4
hott/algebra/category/basic.hlean
View file

@ -12,7 +12,7 @@ open precategory morphism is_equiv eq truncation nat sigma sigma.ops
structure category [class] (ob : Type) extends (precategory ob) := 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)) (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 namespace category
variables {ob : Type} {C : category ob} {a b : ob} variables {ob : Type} {C : category ob} {a b : ob}
@ -20,7 +20,7 @@ namespace category
-- Make iso_of_path_equiv a class instance -- Make iso_of_path_equiv a class instance
-- TODO: Unsafe 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 := definition path_of_iso {a b : ob} : a ≅ b → a = b :=
iso_of_path⁻¹ iso_of_path⁻¹

2
hott/algebra/category/set.hlean
View file

@ -29,7 +29,7 @@ end precategory
namespace category namespace category
universe variable l 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)) definition set_category_equiv_iso (a b : (Σ (A : Type.{l}), is_hset A))
: (a ≅ b) = (a.1 ≃ b.1) := : (a ≅ b) = (a.1 ≃ b.1) :=

48
hott/algebra/group.hlean
View file

@ -493,73 +493,73 @@ end add_comm_group
structure Semigroup := structure Semigroup :=
(carrier : Type) (struct : semigroup carrier) (carrier : Type) (struct : semigroup carrier)
persistent attribute Semigroup.carrier [coercion] attribute Semigroup.carrier [coercion]
persistent attribute Semigroup.struct [instance] attribute Semigroup.struct [instance]
structure CommSemigroup := structure CommSemigroup :=
(carrier : Type) (struct : comm_semigroup carrier) (carrier : Type) (struct : comm_semigroup carrier)
persistent attribute CommSemigroup.carrier [coercion] attribute CommSemigroup.carrier [coercion]
persistent attribute CommSemigroup.struct [instance] attribute CommSemigroup.struct [instance]
structure Monoid := structure Monoid :=
(carrier : Type) (struct : monoid carrier) (carrier : Type) (struct : monoid carrier)
persistent attribute Monoid.carrier [coercion] attribute Monoid.carrier [coercion]
persistent attribute Monoid.struct [instance] attribute Monoid.struct [instance]
structure CommMonoid := structure CommMonoid :=
(carrier : Type) (struct : comm_monoid carrier) (carrier : Type) (struct : comm_monoid carrier)
persistent attribute CommMonoid.carrier [coercion] attribute CommMonoid.carrier [coercion]
persistent attribute CommMonoid.struct [instance] attribute CommMonoid.struct [instance]
structure Group := structure Group :=
(carrier : Type) (struct : group carrier) (carrier : Type) (struct : group carrier)
persistent attribute Group.carrier [coercion] attribute Group.carrier [coercion]
persistent attribute Group.struct [instance] attribute Group.struct [instance]
structure CommGroup := structure CommGroup :=
(carrier : Type) (struct : comm_group carrier) (carrier : Type) (struct : comm_group carrier)
persistent attribute CommGroup.carrier [coercion] attribute CommGroup.carrier [coercion]
persistent attribute CommGroup.struct [instance] attribute CommGroup.struct [instance]
structure AddSemigroup := structure AddSemigroup :=
(carrier : Type) (struct : add_semigroup carrier) (carrier : Type) (struct : add_semigroup carrier)
persistent attribute AddSemigroup.carrier [coercion] attribute AddSemigroup.carrier [coercion]
persistent attribute AddSemigroup.struct [instance] attribute AddSemigroup.struct [instance]
structure AddCommSemigroup := structure AddCommSemigroup :=
(carrier : Type) (struct : add_comm_semigroup carrier) (carrier : Type) (struct : add_comm_semigroup carrier)
persistent attribute AddCommSemigroup.carrier [coercion] attribute AddCommSemigroup.carrier [coercion]
persistent attribute AddCommSemigroup.struct [instance] attribute AddCommSemigroup.struct [instance]
structure AddMonoid := structure AddMonoid :=
(carrier : Type) (struct : add_monoid carrier) (carrier : Type) (struct : add_monoid carrier)
persistent attribute AddMonoid.carrier [coercion] attribute AddMonoid.carrier [coercion]
persistent attribute AddMonoid.struct [instance] attribute AddMonoid.struct [instance]
structure AddCommMonoid := structure AddCommMonoid :=
(carrier : Type) (struct : add_comm_monoid carrier) (carrier : Type) (struct : add_comm_monoid carrier)
persistent attribute AddCommMonoid.carrier [coercion] attribute AddCommMonoid.carrier [coercion]
persistent attribute AddCommMonoid.struct [instance] attribute AddCommMonoid.struct [instance]
structure AddGroup := structure AddGroup :=
(carrier : Type) (struct : add_group carrier) (carrier : Type) (struct : add_group carrier)
persistent attribute AddGroup.carrier [coercion] attribute AddGroup.carrier [coercion]
persistent attribute AddGroup.struct [instance] attribute AddGroup.struct [instance]
structure AddCommGroup := structure AddCommGroup :=
(carrier : Type) (struct : add_comm_group carrier) (carrier : Type) (struct : add_comm_group carrier)
persistent attribute AddCommGroup.carrier [coercion] attribute AddCommGroup.carrier [coercion]
persistent attribute AddCommGroup.struct [instance] attribute AddCommGroup.struct [instance]
end path_algebra end path_algebra

2
hott/algebra/groupoid.hlean
View file

@ -14,7 +14,7 @@ structure groupoid [class] (ob : Type) extends precategory ob :=
namespace groupoid namespace groupoid
persistent attribute all_iso [instance] attribute all_iso [instance]
--set_option pp.universes true --set_option pp.universes true
--set_option pp.implicit true --set_option pp.implicit true

4
hott/algebra/precategory/basic.hlean
View file

@ -14,13 +14,13 @@ structure precategory [class] (ob : Type) : Type :=
(id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f) (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) (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
persistent attribute precategory [multiple-instances] attribute precategory [multiple-instances]
namespace precategory namespace precategory
variables {ob : Type} [C : precategory ob] variables {ob : Type} [C : precategory ob]
variables {a b c d : ob} variables {a b c d : ob}
include C include C
persistent attribute homH [instance] attribute homH [instance]
definition compose := comp definition compose := comp

4
hott/algebra/precategory/constructions.hlean
View file

@ -110,7 +110,7 @@ namespace precategory
infixr `×c`:30 := product.Prod_precategory infixr `×c`:30 := product.Prod_precategory
--instance [persistent] type_category category_one --instance [persistent] type_category category_one
-- category_two product.prod_category -- category_two product.prod_category
persistent attribute product.prod_precategory [instance] attribute product.prod_precategory [instance]
end ops end ops
@ -218,7 +218,7 @@ namespace precategory
exit exit
definition Slice_category [reducible] (C : Category) (c : C) := Mk (slice_category C c) definition Slice_category [reducible] (C : Category) (c : C) := Mk (slice_category C c)
open category.ops open category.ops
instance [persistent] slice_category attribute slice_category [instance]
variables {D : Category} variables {D : Category}
definition forgetful (x : D) : (Slice_category D x) ⇒ D := definition forgetful (x : D) : (Slice_category D x) ⇒ D :=
functor.mk (λ a, to_ob a) functor.mk (λ a, to_ob a)

6
hott/algebra/precategory/functor.hlean
View file

@ -19,8 +19,8 @@ infixl `⇒`:25 := functor
namespace functor namespace functor
variables {C D E : Precategory} variables {C D E : Precategory}
persistent attribute obF [coercion] attribute obF [coercion]
persistent attribute homF [coercion] attribute homF [coercion]
-- "functor C D" is equivalent to a certain sigma type -- "functor C D" is equivalent to a certain sigma type
set_option unifier.max_steps 38500 set_option unifier.max_steps 38500
@ -156,7 +156,7 @@ namespace precategory
namespace ops namespace ops
notation `PreCat`:max := Precat_of_strict_cats notation `PreCat`:max := Precat_of_strict_cats
persistent attribute precat_of_strict_precats [instance] attribute precat_of_strict_precats [instance]
end ops end ops

4
hott/algebra/precategory/morphism.hlean
View file

@ -16,7 +16,7 @@ namespace morphism
inductive is_iso [class] (f : a ⟶ b) : Type inductive is_iso [class] (f : a ⟶ b) : Type
:= mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f := 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 := definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
is_section.rec (λg h, g) H is_section.rec (λg h, g) H
@ -133,7 +133,7 @@ namespace morphism
namespace isomorphic namespace isomorphic
-- openrelation -- openrelation
persistent attribute is_iso [instance] attribute is_iso [instance]
definition refl (a : ob) : a ≅ a := definition refl (a : ob) : a ≅ a :=
mk id mk id

2
hott/init/axioms/funext_varieties.hlean
View file

@ -85,7 +85,7 @@ context
@transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f idhtpy) (sigma.mk g h) @transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f idhtpy) (sigma.mk g h)
(@path_contr _ contr_basedhtpy _ _) d (@path_contr _ contr_basedhtpy _ _) d
attribute htpy_ind [reducible] local attribute htpy_ind [reducible]
definition htpy_ind_beta : htpy_ind f idhtpy = d := definition htpy_ind_beta : htpy_ind f idhtpy = d :=
(@path2_contr _ _ _ _ !path_contr idp)⁻¹ ▹ idp (@path2_contr _ _ _ _ !path_contr idp)⁻¹ ▹ idp

2
hott/init/equiv.hlean
View file

@ -212,7 +212,7 @@ end is_equiv
namespace equiv namespace equiv
persistent attribute to_is_equiv [instance] attribute to_is_equiv [instance]
infix `≃`:25 := equiv infix `≃`:25 := equiv

2
hott/init/hedberg.hlean
View file

@ -43,4 +43,4 @@ context
... = q : aux) ... = q : aux)
end end
persistent attribute is_hset_of_decidable_eq [instance] attribute is_hset_of_decidable_eq [instance]

2
hott/init/nat.hlean
View file

@ -296,7 +296,7 @@ namespace nat
notation a * b := mul a b 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 := definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
rec_on b rec_on b
rfl rfl

2
hott/init/trunc.hlean
View file

@ -188,7 +188,7 @@ namespace truncation
structure trunctype (n : trunc_index) := structure trunctype (n : trunc_index) :=
(trunctype_type : Type) (is_trunc_trunctype_type : is_trunc n trunctype_type) (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 n `-Type` := trunctype n
notation `hprop` := -1-Type notation `hprop` := -1-Type

2
hott/types/sigma.hlean
View file

@ -142,7 +142,7 @@ namespace sigma
apply dpair_eq_dpair_pp_pp apply dpair_eq_dpair_pp_pp
end 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') : 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 := dpair_eq_dpair p q = dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q :=
begin begin

2
library/algebra/category/basic.lean
View file

@ -19,7 +19,7 @@ structure category [class] (ob : Type) : Type :=
(id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f) (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) (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
persistent attribute category [multiple-instances] attribute category [multiple-instances]
namespace category namespace category
variables {ob : Type} [C : category ob] variables {ob : Type} [C : category ob]

14
library/algebra/category/constructions.lean
View file

@ -77,10 +77,10 @@ namespace category
(λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _) (λ 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) _ _ _)
(λ 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) definition Discrete_category (A : Type) [H : decidable_eq A] := Mk (discrete_category A)
context context
attribute discrete_category [instance] local attribute discrete_category [instance]
include H include H
theorem dicrete_category.endomorphism {a b : A} (f : a ⟶ b) : a = b := 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 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 notation 2 := Category_two
postfix `ᵒᵖ`:max := opposite.Opposite postfix `ᵒᵖ`:max := opposite.Opposite
infixr `×c`:30 := product.Prod_category infixr `×c`:30 := product.Prod_category
persistent attribute type_category [instance] attribute type_category [instance]
persistent attribute category_one [instance] attribute category_one [instance]
persistent attribute category_two [instance] attribute category_two [instance]
persistent attribute product.prod_category [instance] attribute product.prod_category [instance]
end ops end ops
open ops open ops
@ -228,7 +228,7 @@ namespace category
definition Slice_category [reducible] (C : Category) (c : C) := Mk (slice_category C c) definition Slice_category [reducible] (C : Category) (c : C) := Mk (slice_category C c)
open category.ops open category.ops
persistent attribute slice_category [instance] attribute slice_category [instance]
variables {D : Category} variables {D : Category}
definition forgetful (x : D) : (Slice_category D x) ⇒ D := definition forgetful (x : D) : (Slice_category D x) ⇒ D :=
functor.mk (λ a, to_ob a) functor.mk (λ a, to_ob a)

10
library/algebra/category/functor.lean
View file

@ -21,10 +21,10 @@ structure functor (C D : Category) : Type :=
infixl `⇒`:25 := functor infixl `⇒`:25 := functor
namespace functor namespace functor
persistent attribute object [coercion] attribute object [coercion]
persistent attribute morphism [coercion] attribute morphism [coercion]
persistent attribute respect_id [irreducible] attribute respect_id [irreducible]
persistent attribute respect_comp [irreducible] attribute respect_comp [irreducible]
variables {A B C D : Category} variables {A B C D : Category}
@ -71,7 +71,7 @@ namespace category
namespace ops namespace ops
notation `Cat`:max := Category_of_categories notation `Cat`:max := Category_of_categories
persistent attribute category_of_categories [instance] attribute category_of_categories [instance]
end ops end ops
end category end category

4
library/algebra/category/morphism.lean
View file

@ -20,7 +20,7 @@ namespace morphism
inductive is_iso [class] (f : a ⟶ b) : Type inductive is_iso [class] (f : a ⟶ b) : Type
:= mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f := 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 := definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
is_section.rec (λg h, g) H is_section.rec (λg h, g) H
@ -131,7 +131,7 @@ namespace morphism
namespace isomorphic namespace isomorphic
open relation open relation
persistent attribute is_iso [instance] attribute is_iso [instance]
theorem refl (a : ob) : a ≅ a := mk id theorem refl (a : ob) : a ≅ a := mk id
theorem symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := mk (inverse (iso H)) theorem symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := mk (inverse (iso H))

48
library/algebra/group.lean
View file

@ -489,73 +489,73 @@ end add_comm_group
structure Semigroup := structure Semigroup :=
(carrier : Type) (struct : semigroup carrier) (carrier : Type) (struct : semigroup carrier)
persistent attribute Semigroup.carrier [coercion] attribute Semigroup.carrier [coercion]
persistent attribute Semigroup.struct [instance] attribute Semigroup.struct [instance]
structure CommSemigroup := structure CommSemigroup :=
(carrier : Type) (struct : comm_semigroup carrier) (carrier : Type) (struct : comm_semigroup carrier)
persistent attribute CommSemigroup.carrier [coercion] attribute CommSemigroup.carrier [coercion]
persistent attribute CommSemigroup.struct [instance] attribute CommSemigroup.struct [instance]
structure Monoid := structure Monoid :=
(carrier : Type) (struct : monoid carrier) (carrier : Type) (struct : monoid carrier)
persistent attribute Monoid.carrier [coercion] attribute Monoid.carrier [coercion]
persistent attribute Monoid.struct [instance] attribute Monoid.struct [instance]
structure CommMonoid := structure CommMonoid :=
(carrier : Type) (struct : comm_monoid carrier) (carrier : Type) (struct : comm_monoid carrier)
persistent attribute CommMonoid.carrier [coercion] attribute CommMonoid.carrier [coercion]
persistent attribute CommMonoid.struct [instance] attribute CommMonoid.struct [instance]
structure Group := structure Group :=
(carrier : Type) (struct : group carrier) (carrier : Type) (struct : group carrier)
persistent attribute Group.carrier [coercion] attribute Group.carrier [coercion]
persistent attribute Group.struct [instance] attribute Group.struct [instance]
structure CommGroup := structure CommGroup :=
(carrier : Type) (struct : comm_group carrier) (carrier : Type) (struct : comm_group carrier)
persistent attribute CommGroup.carrier [coercion] attribute CommGroup.carrier [coercion]
persistent attribute CommGroup.struct [instance] attribute CommGroup.struct [instance]
structure AddSemigroup := structure AddSemigroup :=
(carrier : Type) (struct : add_semigroup carrier) (carrier : Type) (struct : add_semigroup carrier)
persistent attribute AddSemigroup.carrier [coercion] attribute AddSemigroup.carrier [coercion]
persistent attribute AddSemigroup.struct [instance] attribute AddSemigroup.struct [instance]
structure AddCommSemigroup := structure AddCommSemigroup :=
(carrier : Type) (struct : add_comm_semigroup carrier) (carrier : Type) (struct : add_comm_semigroup carrier)
persistent attribute AddCommSemigroup.carrier [coercion] attribute AddCommSemigroup.carrier [coercion]
persistent attribute AddCommSemigroup.struct [instance] attribute AddCommSemigroup.struct [instance]
structure AddMonoid := structure AddMonoid :=
(carrier : Type) (struct : add_monoid carrier) (carrier : Type) (struct : add_monoid carrier)
persistent attribute AddMonoid.carrier [coercion] attribute AddMonoid.carrier [coercion]
persistent attribute AddMonoid.struct [instance] attribute AddMonoid.struct [instance]
structure AddCommMonoid := structure AddCommMonoid :=
(carrier : Type) (struct : add_comm_monoid carrier) (carrier : Type) (struct : add_comm_monoid carrier)
persistent attribute AddCommMonoid.carrier [coercion] attribute AddCommMonoid.carrier [coercion]
persistent attribute AddCommMonoid.struct [instance] attribute AddCommMonoid.struct [instance]
structure AddGroup := structure AddGroup :=
(carrier : Type) (struct : add_group carrier) (carrier : Type) (struct : add_group carrier)
persistent attribute AddGroup.carrier [coercion] attribute AddGroup.carrier [coercion]
persistent attribute AddGroup.struct [instance] attribute AddGroup.struct [instance]
structure AddCommGroup := structure AddCommGroup :=
(carrier : Type) (struct : add_comm_group carrier) (carrier : Type) (struct : add_comm_group carrier)
persistent attribute AddCommGroup.carrier [coercion] attribute AddCommGroup.carrier [coercion]
persistent attribute AddCommGroup.struct [instance] attribute AddCommGroup.struct [instance]
end algebra end algebra

4
library/data/bool.lean
View file

@ -10,8 +10,8 @@ import logic.eq
open eq eq.ops decidable open eq eq.ops decidable
namespace bool namespace bool
attribute bor [reducible] local attribute bor [reducible]
attribute band [reducible] local attribute band [reducible]
theorem dichotomy (b : bool) : b = ff ∨ b = tt := theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
cases_on b (or.inl rfl) (or.inr rfl) cases_on b (or.inl rfl) (or.inr rfl)

2
library/data/int/basic.lean
View file

@ -42,7 +42,7 @@ inductive int : Type :=
neg_succ_of_nat : nat → int neg_succ_of_nat : nat → int
notation `ℤ` := 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) definition int.of_num [coercion] [reducible] (n : num) : ℤ := int.of_nat (nat.of_num n)
namespace int namespace int

4
library/data/list/basic.lean
View file

@ -197,8 +197,8 @@ induction_on s
theorem mem_concat (x : T) (s t : list T) : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t := 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 iff.intro mem_concat_imp_or mem_or_imp_concat
attribute mem [reducible] local attribute mem [reducible]
attribute append [reducible] local attribute append [reducible]
theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) := theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) :=
induction_on l induction_on l
(take H : x ∈ nil, false.elim (iff.elim_left !mem_nil H)) (take H : x ∈ nil, false.elim (iff.elim_left !mem_nil H))

2
library/data/nat/div.lean
View file

@ -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 := 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 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 infixl [local] `≺`:50 := pair_nat.lt
private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) := private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) :=

2
library/init/nat.lean
View file

@ -288,7 +288,7 @@ namespace nat
notation a * b := mul a b notation a * b := mul a b
section context
attribute sub [reducible] attribute sub [reducible]
definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b := definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
induction_on b induction_on b

2
src/emacs/lean-syntax.el
View file

@ -16,7 +16,7 @@
"calc_trans" "calc_subst" "calc_refl" "calc_symm" "match" "calc_trans" "calc_subst" "calc_refl" "calc_symm" "match"
"infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
"using" "namespace" "section" "fields" "find_decl" "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") "instances" "coercions" "raw")
"lean keywords") "lean keywords")

10
src/frontends/lean/builtin_cmds.cpp
View file

@ -575,6 +575,15 @@ environment telescope_eq_cmd(parser & p) {
return p.env(); 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) { void init_cmd_table(cmd_table & r) {
add_cmd(r, cmd_info("open", "create aliases for declarations, and use objects defined in other namespaces", add_cmd(r, cmd_info("open", "create aliases for declarations, and use objects defined in other namespaces",
open_cmd)); 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("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("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("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("#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("#projections", "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd)); add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd));

8
src/frontends/lean/decl_cmds.cpp
View file

@ -1015,12 +1015,11 @@ static environment attribute_cmd_core(parser & p, bool persistent) {
} }
static environment attribute_cmd(parser & p) { 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) { environment local_attribute_cmd(parser & p) {
p.check_token_next(get_attribute_tk(), "invalid command, 'attribute' expected"); return attribute_cmd_core(p, false);
return attribute_cmd_core(p, true);
} }
void register_decl_cmds(cmd_table & r) { 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("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("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("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)); add_cmd(r, cmd_info("omit", "undo 'include' command", omit_cmd));
} }
} }

6
src/frontends/lean/decl_cmds.h
View file

@ -17,10 +17,12 @@ class parser;
*/ */
bool parse_univ_params(parser & p, buffer<name> & ps); bool parse_univ_params(parser & p, buffer<name> & ps);
expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos); 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). Then sort \c ls_buffer (using the order in which the universe levels were declared).
*/ */
void update_univ_parameters(buffer<name> & ls_buffer, name_set const & found_ls, parser const & p); void update_univ_parameters(buffer<name> & 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); void register_decl_cmds(cmd_table & r);
} }

5
src/frontends/lean/notation_cmd.cpp
View file

@ -685,6 +685,11 @@ static environment prefix_cmd(parser & p) {
return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve); 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) { static environment reserve_cmd(parser & p) {
bool overload = false; bool overload = false;
bool reserve = true; bool reserve = true;

3
src/frontends/lean/notation_cmd.h
View file

@ -17,5 +17,8 @@ bool curr_is_notation_decl(parser & p);
*/ */
notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & new_tokens, bool allow_local); notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & new_tokens, bool allow_local);
/** \brief Parse local notation */
environment local_notation_cmd(parser & p);
void register_notation_cmds(cmd_table & r); void register_notation_cmds(cmd_table & r);
} }

4
src/frontends/lean/token_table.cpp
View file

@ -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}, {"(*", 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}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
{"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0}, {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},
{"<d", g_decreasing_prec}, {"local", 0}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}}; {"<d", g_decreasing_prec}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
char const * commands[] = char const * commands[] =
{"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion", {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
"[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[parsing-only]", "[multiple-instances]", "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[parsing-only]", "[multiple-instances]",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "prelude", "evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "prelude",
"import", "inductive", "record", "structure", "module", "universe", "universes", "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context", "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
"exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint", "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
"add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent", "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent",

2
tests/lean/run/e6.lean
View file

@ -13,7 +13,7 @@ namespace int
constant add : int → int → int constant add : int → int → int
infixl + := add infixl + := add
constant of_nat : nat → int constant of_nat : nat → int
persistent attribute of_nat [coercion] attribute of_nat [coercion]
end int end int
open int open int

2
tests/lean/run/e9.lean
View file

@ -16,7 +16,7 @@ namespace int
end int end int
namespace int_coercions namespace int_coercions
persistent attribute int.of_nat [coercion] attribute int.of_nat [coercion]
end int_coercions end int_coercions
-- Open "only" the notation and declarations from the namespaces nat and int -- Open "only" the notation and declarations from the namespaces nat and int

2
tests/lean/run/fibrant_class1.lean
View file

@ -7,7 +7,7 @@ idpath : path a a
notation a ≈ b := path a b notation a ≈ b := path a b
axiom path_fibrant {A : Type'} [fA : fibrant A] (a b : A) : fibrant (path a b) axiom path_fibrant {A : Type'} [fA : fibrant A] (a b : A) : fibrant (path a b)
persistent attribute path_fibrant [instance] attribute path_fibrant [instance]
axiom imp_fibrant {A : Type'} {B : Type'} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A → B) axiom imp_fibrant {A : Type'} {B : Type'} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A → B)
attribute imp_fibrant [instance] attribute imp_fibrant [instance]

2
tests/lean/run/fibrant_class2.lean
View file

@ -9,7 +9,7 @@ inductive path {A : Type} [fA : fibrant A] (a : A) : A → Type :=
idpath : path a a idpath : path a a
axiom path_fibrant {A : Type} [fA : fibrant A] (a b : A) : fibrant (path a b) axiom path_fibrant {A : Type} [fA : fibrant A] (a b : A) : fibrant (path a b)
persistent attribute path_fibrant [instance] attribute path_fibrant [instance]
notation a ≈ b := path a b notation a ≈ b := path a b

16
tests/lean/run/group4.lean
View file

@ -80,26 +80,26 @@ print prefix algebra.comm_monoid
structure Semigroup := structure Semigroup :=
mk :: (carrier : Type) (struct : semigroup carrier) mk :: (carrier : Type) (struct : semigroup carrier)
persistent attribute Semigroup.carrier [coercion] attribute Semigroup.carrier [coercion]
persistent attribute Semigroup.struct [instance] attribute Semigroup.struct [instance]
structure CommSemigroup := structure CommSemigroup :=
mk :: (carrier : Type) (struct : comm_semigroup carrier) mk :: (carrier : Type) (struct : comm_semigroup carrier)
persistent attribute CommSemigroup.carrier [coercion] attribute CommSemigroup.carrier [coercion]
persistent attribute CommSemigroup.struct [instance] attribute CommSemigroup.struct [instance]
structure Monoid := structure Monoid :=
mk :: (carrier : Type) (struct : monoid carrier) mk :: (carrier : Type) (struct : monoid carrier)
persistent attribute Monoid.carrier [coercion] attribute Monoid.carrier [coercion]
persistent attribute Monoid.struct [instance] attribute Monoid.struct [instance]
structure CommMonoid := structure CommMonoid :=
mk :: (carrier : Type) (struct : comm_monoid carrier) mk :: (carrier : Type) (struct : comm_monoid carrier)
persistent attribute CommMonoid.carrier [coercion] attribute CommMonoid.carrier [coercion]
persistent attribute CommMonoid.struct [instance] attribute CommMonoid.struct [instance]
end algebra end algebra

16
tests/lean/run/group5.lean
View file

@ -78,26 +78,26 @@ structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
structure Semigroup := structure Semigroup :=
(carrier : Type) (struct : semigroup carrier) (carrier : Type) (struct : semigroup carrier)
persistent attribute Semigroup.carrier [coercion] attribute Semigroup.carrier [coercion]
persistent attribute Semigroup.struct [instance] attribute Semigroup.struct [instance]
structure CommSemigroup := structure CommSemigroup :=
(carrier : Type) (struct : comm_semigroup carrier) (carrier : Type) (struct : comm_semigroup carrier)
persistent attribute CommSemigroup.carrier [coercion] attribute CommSemigroup.carrier [coercion]
persistent attribute CommSemigroup.struct [instance] attribute CommSemigroup.struct [instance]
structure Monoid := structure Monoid :=
(carrier : Type) (struct : monoid carrier) (carrier : Type) (struct : monoid carrier)
persistent attribute Monoid.carrier [coercion] attribute Monoid.carrier [coercion]
persistent attribute Monoid.struct [instance] attribute Monoid.struct [instance]
structure CommMonoid := structure CommMonoid :=
(carrier : Type) (struct : comm_monoid carrier) (carrier : Type) (struct : comm_monoid carrier)
persistent attribute CommMonoid.carrier [coercion] attribute CommMonoid.carrier [coercion]
persistent attribute CommMonoid.struct [instance] attribute CommMonoid.struct [instance]
end algebra end algebra