From f00e6c0a9666d335f75ecf73291bb13225aee285 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Sep 2016 13:34:34 -0700 Subject: [PATCH] feat(frontends/lean): anonymous instances The instance name is synthesized automatically. --- library/init/char.lean | 8 +-- library/init/coe.lean | 57 +++++++--------- library/init/datatypes.lean | 72 ++++++--------------- library/init/fin.lean | 3 +- library/init/instances.lean | 10 +-- library/init/list.lean | 6 +- library/init/list_classes.lean | 6 +- library/init/logic.lean | 55 ++++++---------- library/init/nat.lean | 15 ++--- library/init/nat_div.lean | 6 +- library/init/num.lean | 9 +-- library/init/option.lean | 20 ++---- library/init/ordering.lean | 15 ++--- library/init/prod.lean | 6 +- library/init/quot.lean | 3 +- library/init/set.lean | 9 +-- library/init/simplifier.lean | 6 +- library/init/state.lean | 10 ++- library/init/string.lean | 3 +- library/init/subtype.lean | 5 +- library/init/sum.lean | 6 +- library/init/to_string.lean | 43 ++++-------- library/init/unit.lean | 6 +- library/init/unsigned.lean | 5 +- src/emacs/lean-syntax.el | 8 +-- src/frontends/lean/decl_attributes.cpp | 7 +- src/frontends/lean/decl_attributes.h | 6 +- src/frontends/lean/decl_cmds.cpp | 4 +- src/frontends/lean/decl_util.cpp | 29 +++++++-- src/frontends/lean/decl_util.h | 3 +- src/frontends/lean/definition_cmds.cpp | 9 ++- src/library/constants.cpp | 56 ++++++++-------- src/library/constants.txt | 56 ++++++++-------- tests/lean/584a.lean.expected.out | 4 +- tests/lean/attributes.lean | 2 +- tests/lean/coe4.lean.expected.out | 2 +- tests/lean/defeq_simp1.lean | 4 +- tests/lean/elab2.lean.expected.out | 4 +- tests/lean/elab7.lean.expected.out | 8 +-- tests/lean/elab9.lean.expected.out | 4 +- tests/lean/eta_tac.lean.expected.out | 4 +- tests/lean/pp_all.lean.expected.out | 6 +- tests/lean/pp_all2.lean.expected.out | 2 +- tests/lean/qexpr1.lean.expected.out | 4 +- tests/lean/qexpr2.lean.expected.out | 4 +- tests/lean/run/968.lean | 6 +- tests/lean/run/stateT1.lean | 3 +- tests/lean/set_opt_tac.lean.expected.out | 2 +- tests/lean/type_class_bug.lean.expected.out | 20 +++--- 49 files changed, 270 insertions(+), 371 deletions(-) diff --git a/library/init/char.lean b/library/init/char.lean index 09ae6b8630..c9c6363968 100644 --- a/library/init/char.lean +++ b/library/init/char.lean @@ -24,11 +24,9 @@ def to_nat (c : char) : nat := fin.val c end char -attribute [instance] -def char_has_decidable_eq : decidable_eq char := -have decidable_eq (fin char_sz), from fin.has_decidable_eq _, +instance : decidable_eq char := +have decidable_eq (fin char_sz), from fin.decidable_eq _, this -attribute [instance] -def char_is_inhabited : inhabited char := +instance : inhabited char := ⟨'A'⟩ diff --git a/library/init/coe.lean b/library/init/coe.lean index 110cdfbb6b..c6ac5f3c4a 100644 --- a/library/init/coe.lean +++ b/library/init/coe.lean @@ -82,80 +82,67 @@ notation `⇑`:max a:max := coe_fn a notation `↥`:max a:max := coe_sort a +universe variables u₁ u₂ u₃ + /- Transitive closure for has_lift, has_coe, has_coe_to_fun -/ -attribute [instance] -def {u₁ u₂ u₃} lift_trans {A : Type u₁} {B : Type u₂} {C : Type u₃} [has_lift A B] [has_lift_t B C] : has_lift_t A C := +instance lift_trans {A : Type u₁} {B : Type u₂} {C : Type u₃} [has_lift A B] [has_lift_t B C] : has_lift_t A C := ⟨λ a, lift_t (lift a : B)⟩ -attribute [instance] -def lift_base {A : Type u} {B : Type v} [has_lift A B] : has_lift_t A B := +instance lift_base {A : Type u} {B : Type v} [has_lift A B] : has_lift_t A B := ⟨lift⟩ -attribute [instance] -def {u₁ u₂ u₃} coe_trans {A : Type u₁} {B : Type u₂} {C : Type u₃} [has_coe A B] [has_coe_t B C] : has_coe_t A C := +instance coe_trans {A : Type u₁} {B : Type u₂} {C : Type u₃} [has_coe A B] [has_coe_t B C] : has_coe_t A C := ⟨λ a, coe_t (coe_b a : B)⟩ -attribute [instance] -def coe_base {A : Type u} {B : Type v} [has_coe A B] : has_coe_t A B := +instance coe_base {A : Type u} {B : Type v} [has_coe A B] : has_coe_t A B := ⟨coe_b⟩ -attribute [instance] -def {u₁ u₂ u₃} coe_fn_trans {A : Type u₁} {B : Type u₂} [has_lift_t A B] [has_coe_to_fun.{u₂ u₃} B] : has_coe_to_fun.{u₁ u₃} A := +instance coe_fn_trans {A : Type u₁} {B : Type u₂} [has_lift_t A B] [has_coe_to_fun.{u₂ u₃} B] : has_coe_to_fun.{u₁ u₃} A := ⟨has_coe_to_fun.F B, λ a, coe_fn (coe a)⟩ -attribute [instance] -def {u₁ u₂ u₃} coe_sort_trans {A : Type u₁} {B : Type u₂} [has_lift_t A B] [has_coe_to_sort.{u₂ u₃} B] : has_coe_to_sort.{u₁ u₃} A := +instance coe_sort_trans {A : Type u₁} {B : Type u₂} [has_lift_t A B] [has_coe_to_sort.{u₂ u₃} B] : has_coe_to_sort.{u₁ u₃} A := ⟨has_coe_to_sort.S B, λ a, coe_sort (coe a)⟩ /- Every coercion is also a lift -/ -attribute [instance] -def coe_to_lift {A : Type u} {B : Type v} [has_coe_t A B] : has_lift_t A B := +instance coe_to_lift {A : Type u} {B : Type v} [has_coe_t A B] : has_lift_t A B := ⟨coe_t⟩ /- Basic coercions -/ -attribute [instance] -def coe_bool_to_Prop : has_coe bool Prop := +instance coe_bool_to_Prop : has_coe bool Prop := ⟨λ b, b = tt⟩ -attribute [instance] -def coe_decidable_eq (b : bool) : decidable (coe b) := -show decidable (b = tt), from bool.has_decidable_eq b tt +instance coe_decidable_eq (b : bool) : decidable (coe b) := +show decidable (b = tt), from bool.decidable_eq b tt -attribute [instance] -def coe_subtype {A : Type u} {p : A → Prop} : has_coe {a // p a} A := +instance coe_subtype {A : Type u} {p : A → Prop} : has_coe {a // p a} A := ⟨λ s, subtype.elt_of s⟩ /- Basic lifts -/ +universe variables ua ua₁ ua₂ ub ub₁ ub₂ + /- Remark: we can't use [has_lift_t A₂ A₁] since it will produce non-termination whenever a type class resolution problem does not have a solution. -/ -attribute [instance] -def {ua₁ ua₂ ub₁ ub₂} lift_fn {A₁ : Type ua₁} {A₂ : Type ua₂} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift A₂ A₁] [has_lift_t B₁ B₂] : has_lift (A₁ → B₁) (A₂ → B₂) := +instance lift_fn {A₁ : Type ua₁} {A₂ : Type ua₂} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift A₂ A₁] [has_lift_t B₁ B₂] : has_lift (A₁ → B₁) (A₂ → B₂) := ⟨λ f a, ↑(f ↑a)⟩ -attribute [instance] -def {ua ub₁ ub₂} lift_fn_range {A : Type ua} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift_t B₁ B₂] : has_lift (A → B₁) (A → B₂) := +instance lift_fn_range {A : Type ua} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift_t B₁ B₂] : has_lift (A → B₁) (A → B₂) := ⟨λ f a, ↑(f a)⟩ -attribute [instance] -def {ua₁ ua₂ ub} lift_fn_dom {A₁ : Type ua₁} {A₂ : Type ua₂} {B : Type ub} [has_lift A₂ A₁] : has_lift (A₁ → B) (A₂ → B) := +instance lift_fn_dom {A₁ : Type ua₁} {A₂ : Type ua₂} {B : Type ub} [has_lift A₂ A₁] : has_lift (A₁ → B) (A₂ → B) := ⟨λ f a, f ↑a⟩ -attribute [instance] -def {ua₁ ua₂ ub₁ ub₂} lift_pair {A₁ : Type ua₁} {A₂ : Type ub₂} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift_t A₁ A₂] [has_lift_t B₁ B₂] : has_lift (A₁ × B₁) (A₂ × B₂) := +instance lift_pair {A₁ : Type ua₁} {A₂ : Type ub₂} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift_t A₁ A₂] [has_lift_t B₁ B₂] : has_lift (A₁ × B₁) (A₂ × B₂) := ⟨λ p, prod.cases_on p (λ a b, (↑a, ↑b))⟩ -attribute [instance] -def {ua₁ ua₂ ub} lift_pair₁ {A₁ : Type ua₁} {A₂ : Type ua₂} {B : Type ub} [has_lift_t A₁ A₂] : has_lift (A₁ × B) (A₂ × B) := +instance lift_pair₁ {A₁ : Type ua₁} {A₂ : Type ua₂} {B : Type ub} [has_lift_t A₁ A₂] : has_lift (A₁ × B) (A₂ × B) := ⟨λ p, prod.cases_on p (λ a b, (↑a, b))⟩ -attribute [instance] -def {ua ub₁ ub₂} lift_pair₂ {A : Type ua} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift_t B₁ B₂] : has_lift (A × B₁) (A × B₂) := +instance lift_pair₂ {A : Type ua} {B₁ : Type ub₁} {B₂ : Type ub₂} [has_lift_t B₁ B₂] : has_lift (A × B₁) (A × B₂) := ⟨λ p, prod.cases_on p (λ a b, (a, ↑b))⟩ -attribute [instance] -def lift_list {A : Type u} {B : Type v} [has_lift_t A B] : has_lift (list A) (list B) := +instance lift_list {A : Type u} {B : Type v} [has_lift_t A B] : has_lift (list A) (list B) := ⟨λ l, list.map (@coe A B _) l⟩ diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index ded171d792..e34662a479 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -156,16 +156,13 @@ def bit1 {A : Type u} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A := add ( attribute [pattern] zero one bit0 bit1 add -attribute [instance] -def num_has_zero : has_zero num := +instance : has_zero num := ⟨num.zero⟩ -attribute [instance] -def num_has_one : has_one num := +instance : has_one num := ⟨num.pos pos_num.one⟩ -attribute [instance] -def pos_num_has_one : has_one pos_num := +instance : has_one pos_num := ⟨pos_num.one⟩ namespace pos_num @@ -192,8 +189,7 @@ namespace pos_num b end pos_num -attribute [instance] -def pos_num_has_add : has_add pos_num := +instance : has_add pos_num := ⟨pos_num.add⟩ namespace num @@ -203,8 +199,7 @@ namespace num num.rec_on a b (λ pa, num.rec_on b (pos pa) (λ pb, pos (pos_num.add pa pb))) end num -attribute [instance] -def num_has_add : has_add num := +instance : has_add num := ⟨num.add⟩ def std.priority.default : num := 1000 @@ -223,20 +218,11 @@ namespace nat num.rec zero (λ p, of_pos_num p) n end nat -attribute pos_num_has_add pos_num_has_one num_has_zero num_has_one num_has_add - [instance, priority nat.prio] +instance : has_zero nat := ⟨nat.zero⟩ -attribute [instance, priority nat.prio] -def nat_has_zero : has_zero nat := -⟨nat.zero⟩ +instance : has_one nat := ⟨nat.succ (nat.zero)⟩ -attribute [instance, priority nat.prio] -def nat_has_one : has_one nat := -⟨nat.succ (nat.zero)⟩ - -attribute [instance, priority nat.prio] -def nat_has_add : has_add nat := -⟨nat.add⟩ +instance : has_add nat := ⟨nat.add⟩ /- Global declarations of right binding strength @@ -385,32 +371,27 @@ From now on, the inductive compiler will automatically generate sizeof instances -/ /- Every type `A` has a default has_sizeof instance that just returns 0 for every element of `A` -/ -attribute [instance] -def default_has_sizeof (A : Type u) : has_sizeof A := +instance default_has_sizeof (A : Type u) : has_sizeof A := ⟨λ a, nat.zero⟩ attribute [simp, defeq, simp.sizeof] def default_has_sizeof_eq (A : Type u) (a : A) : @sizeof A (default_has_sizeof A) a = 0 := rfl -attribute [instance] -def nat_has_sizeof : has_sizeof nat := -⟨λ a, a⟩ +instance : has_sizeof nat := ⟨λ a, a⟩ attribute [simp, defeq, simp.sizeof] def sizeof_nat_eq (a : nat) : sizeof a = a := rfl -attribute [instance] -def prod_has_sizeof (A : Type u) (B : Type v) [has_sizeof A] [has_sizeof B] : has_sizeof (prod A B) := +instance (A : Type u) (B : Type v) [has_sizeof A] [has_sizeof B] : has_sizeof (prod A B) := ⟨λ p, prod.cases_on p (λ a b, 1 + sizeof a + sizeof b)⟩ attribute [simp, defeq, simp.sizeof] def sizeof_prod_eq {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] (a : A) (b : B) : sizeof (prod.mk a b) = 1 + sizeof a + sizeof b := rfl -attribute [instance] -def sum_has_sizeof (A : Type u) (B : Type v) [has_sizeof A] [has_sizeof B] : has_sizeof (sum A B) := +instance (A : Type u) (B : Type v) [has_sizeof A] [has_sizeof B] : has_sizeof (sum A B) := ⟨λ s, sum.cases_on s (λ a, 1 + sizeof a) (λ b, 1 + sizeof b)⟩ attribute [simp, defeq, simp.sizeof] @@ -421,56 +402,44 @@ attribute [simp, defeq, simp.sizeof] def sizeof_sum_eq_right {A : Type u} {B : Type v} [has_sizeof A] [has_sizeof B] (b : B) : sizeof (@sum.inr A B b) = 1 + sizeof b := rfl -attribute [instance] -def sigma_has_sizeof (A : Type u) (B : A → Type v) [has_sizeof A] [∀ a, has_sizeof (B a)] : has_sizeof (sigma B) := +instance (A : Type u) (B : A → Type v) [has_sizeof A] [∀ a, has_sizeof (B a)] : has_sizeof (sigma B) := ⟨λ p, sigma.cases_on p (λ a b, 1 + sizeof a + sizeof b)⟩ attribute [simp, defeq, simp.sizeof] def sizeof_sigma_eq {A : Type u} {B : A → Type v} [has_sizeof A] [∀ a, has_sizeof (B a)] (a : A) (b : B a) : sizeof (@sigma.mk A B a b) = 1 + sizeof a + sizeof b := rfl -attribute [instance] -def unit_has_sizeof : has_sizeof unit := -⟨λ u, 1⟩ +instance : has_sizeof unit := ⟨λ u, 1⟩ attribute [simp, defeq, simp.sizeof] def sizeof_unit_eq (u : unit) : sizeof u = 1 := rfl -attribute [instance] -def poly_unit_has_sizeof : has_sizeof poly_unit := -⟨λ u, 1⟩ +instance : has_sizeof poly_unit := ⟨λ u, 1⟩ attribute [simp, defeq, simp.sizeof] def sizeof_poly_unit_eq (u : poly_unit) : sizeof u = 1 := rfl -attribute [instance] -def bool_has_sizeof : has_sizeof bool := -⟨λ u, 1⟩ +instance : has_sizeof bool := ⟨λ u, 1⟩ attribute [simp, defeq, simp.sizeof] def sizeof_bool_eq (b : bool) : sizeof b = 1 := rfl -attribute [instance] -def pos_num_has_sizeof : has_sizeof pos_num := -⟨λ p, nat.of_pos_num p⟩ +instance : has_sizeof pos_num := ⟨λ p, nat.of_pos_num p⟩ attribute [simp, defeq, simp.sizeof] def sizeof_pos_num_eq (p : pos_num) : sizeof p = nat.of_pos_num p := rfl -attribute [instance] -def num_has_sizeof : has_sizeof num := -⟨λ p, nat.of_num p⟩ +instance : has_sizeof num := ⟨λ p, nat.of_num p⟩ attribute [simp, defeq, simp.sizeof] def sizeof_num_eq (n : num) : sizeof n = nat.of_num n := rfl -attribute [instance] -def option_has_sizeof (A : Type u) [has_sizeof A] : has_sizeof (option A) := +instance (A : Type u) [has_sizeof A] : has_sizeof (option A) := ⟨λ o, option.cases_on o 1 (λ a, 1 + sizeof a)⟩ attribute [simp, defeq, simp.sizeof] @@ -481,8 +450,7 @@ attribute [simp, defeq, simp.sizeof] def sizeof_option_some_eq {A : Type u} [has_sizeof A] (a : A) : sizeof (some a) = 1 + sizeof a := rfl -attribute [instance] -def list_has_sizeof (A : Type u) [has_sizeof A] : has_sizeof (list A) := +instance (A : Type u) [has_sizeof A] : has_sizeof (list A) := ⟨λ l, list.rec_on l 1 (λ a t ih, 1 + sizeof a + ih)⟩ attribute [simp, defeq, simp.sizeof] diff --git a/library/init/fin.lean b/library/init/fin.lean index 36a14fff59..673402b683 100644 --- a/library/init/fin.lean +++ b/library/init/fin.lean @@ -22,8 +22,7 @@ end fin open fin -attribute [instance] -protected definition fin.has_decidable_eq (n : nat) : ∀ (i j : fin n), decidable (i = j) +instance (n : nat) : decidable_eq (fin n) | ⟨ival, ilt⟩ ⟨jval, jlt⟩ := match nat.has_decidable_eq ival jval with | is_true h₁ := is_true (eq_of_veq h₁) diff --git a/library/init/instances.lean b/library/init/instances.lean index 3eaaef8007..17e27b05d1 100644 --- a/library/init/instances.lean +++ b/library/init/instances.lean @@ -8,17 +8,17 @@ import init.meta.mk_dec_eq_instance init.subtype init.meta.occurrences init.sum open tactic subtype universe variables u v -instance subtype.decidable_eq {A : Type u} {p : A → Prop} [decidable_eq A] : decidable_eq {x : A // p x} := +instance {A : Type u} {p : A → Prop} [decidable_eq A] : decidable_eq {x : A // p x} := by mk_dec_eq_instance -instance list.decidable_eq {A : Type u} [decidable_eq A] : decidable_eq (list A) := +instance {A : Type u} [decidable_eq A] : decidable_eq (list A) := by mk_dec_eq_instance -instance occurrences.decidable_eq : decidable_eq occurrences := +instance : decidable_eq occurrences := by mk_dec_eq_instance -instance unit.decidable_eq : decidable_eq unit := +instance : decidable_eq unit := by mk_dec_eq_instance -instance sum.decidable {A : Type u} {B : Type v} [decidable_eq A] [decidable_eq B] : decidable_eq (A ⊕ B) := +instance {A : Type u} {B : Type v} [decidable_eq A] [decidable_eq B] : decidable_eq (A ⊕ B) := by mk_dec_eq_instance diff --git a/library/init/list.lean b/library/init/list.lean index c01e5aba10..4df0a26a9d 100644 --- a/library/init/list.lean +++ b/library/init/list.lean @@ -9,8 +9,7 @@ open decidable list universe variables u v -attribute [instance] -protected def list.is_inhabited (A : Type u) : inhabited (list A) := +instance (A : Type u) : inhabited (list A) := ⟨list.nil⟩ notation h :: t := cons h t @@ -71,6 +70,5 @@ def dropn : ℕ → list A → list A | (succ n) (x::r) := dropn n r end list -attribute [instance] -def list_has_append {A : Type u} : has_append (list A) := +instance {A : Type u} : has_append (list A) := ⟨list.append⟩ diff --git a/library/init/list_classes.lean b/library/init/list_classes.lean index ea6f011825..d122bfb9bf 100644 --- a/library/init/list_classes.lean +++ b/library/init/list_classes.lean @@ -19,10 +19,8 @@ attribute [inline] def list_return {A : Type u} (a : A) : list A := [a] -attribute [instance] -def list_is_monad : monad list := +instance : monad list := monad.mk @list_fmap @list_return @list_bind -attribute [instance] -def list_is_alternative : alternative list := +instance : alternative list := alternative.mk @list_fmap @list_return (@fapp _ _) @nil @list.append diff --git a/library/init/logic.lean b/library/init/logic.lean index 75af81dbca..baf74c1d4a 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -698,34 +698,28 @@ end section variables {p q : Prop} - attribute [instance] - definition decidable_and [decidable p] [decidable q] : decidable (p ∧ q) := + instance [decidable p] [decidable q] : decidable (p ∧ q) := if hp : p then if hq : q then is_true ⟨hp, hq⟩ else is_false (assume h : p ∧ q, hq (and.right h)) else is_false (assume h : p ∧ q, hp (and.left h)) - attribute [instance] - definition decidable_or [decidable p] [decidable q] : decidable (p ∨ q) := + instance [decidable p] [decidable q] : decidable (p ∨ q) := if hp : p then is_true (or.inl hp) else if hq : q then is_true (or.inr hq) else is_false (or.rec hp hq) - attribute [instance] - definition decidable_not [decidable p] : decidable (¬p) := + instance [decidable p] : decidable (¬p) := if hp : p then is_false (absurd hp) else is_true hp - attribute [instance] - definition decidable_implies [decidable p] [decidable q] : decidable (p → q) := + instance implies.decidable [decidable p] [decidable q] : decidable (p → q) := if hp : p then if hq : q then is_true (assume h, hq) else is_false (assume h : p → q, absurd (h hp) hq) else is_true (assume h, absurd h hp) - attribute [instance] - definition decidable_iff [decidable p] [decidable q] : decidable (p ↔ q) := - decidable_and - + instance [decidable p] [decidable q] : decidable (p ↔ q) := + and.decidable end attribute [reducible] @@ -734,9 +728,9 @@ attribute [reducible] definition decidable_rel {A : Type u} (r : A → A → Prop) := Π (a b : A), decidable (r a b) attribute [reducible] definition decidable_eq (A : Type u) := decidable_rel (@eq A) -attribute [instance] -definition decidable_ne {A : Type u} [decidable_eq A] (a b : A) : decidable (a ≠ b) := -decidable_implies + +instance {A : Type u} [decidable_eq A] (a b : A) : decidable (a ≠ b) := +implies.decidable theorem bool.ff_ne_tt : ff = tt → false . @@ -745,8 +739,7 @@ definition is_dec_eq {A : Type u} (p : A → A → bool) : Prop := ∀ ⦃x y definition is_dec_refl {A : Type u} (p : A → A → bool) : Prop := ∀ x, p x x = tt open decidable -attribute [instance] -protected definition bool.has_decidable_eq : ∀ a b : bool, decidable (a = b) +instance : decidable_eq bool | ff ff := is_true rfl | ff tt := is_false bool.ff_ne_tt | tt ff := is_false (ne.symm bool.ff_ne_tt) @@ -791,29 +784,22 @@ attribute [inline, irreducible] definition arbitrary (A : Type u) [h : inhabited A] : A := inhabited.value h -attribute [instance] -definition Prop.is_inhabited : inhabited Prop := +instance prop.inhabited : inhabited Prop := ⟨true⟩ -attribute [instance] -definition inhabited_fun (A : Type u) {B : Type v} [h : inhabited B] : inhabited (A → B) := +instance fun.inhabited (A : Type u) {B : Type v} [h : inhabited B] : inhabited (A → B) := inhabited.rec_on h (λ b, ⟨λ a, b⟩) -attribute [instance] -definition inhabited_Pi (A : Type u) {B : A → Type v} [Π x, inhabited (B x)] : - inhabited (Π x, B x) := +instance pi.inhabite (A : Type u) {B : A → Type v} [Π x, inhabited (B x)] : inhabited (Π x, B x) := ⟨λ a, default (B a)⟩ -attribute [inline, instance] -protected definition bool.is_inhabited : inhabited bool := +instance : inhabited bool := ⟨ff⟩ -attribute [inline, instance] -protected definition pos_num.is_inhabited : inhabited pos_num := +instance : inhabited pos_num := ⟨pos_num.one⟩ -attribute [inline, instance] -protected definition num.is_inhabited : inhabited num := +instance : inhabited num := ⟨num.zero⟩ inductive [class] nonempty (A : Type u) : Prop @@ -822,8 +808,7 @@ inductive [class] nonempty (A : Type u) : Prop protected definition nonempty.elim {A : Type u} {p : Prop} (h₁ : nonempty A) (h₂ : A → p) : p := nonempty.rec h₂ h₁ -attribute [instance] -theorem nonempty_of_inhabited {A : Type u} [inhabited A] : nonempty A := +instance nonempty_of_inhabited {A : Type u} [inhabited A] : nonempty A := ⟨default A⟩ theorem nonempty_of_exists {A : Type u} {p : A → Prop} : (∃ x, p x) → nonempty A @@ -840,12 +825,10 @@ subsingleton.rec (λ p, p) h protected definition subsingleton.helim {A B : Type u} [h : subsingleton A] (h : A = B) : ∀ (a : A) (b : B), a == b := eq.rec_on h (λ a b : A, heq_of_eq (subsingleton.elim a b)) -attribute [instance] -definition subsingleton_prop (p : Prop) : subsingleton p := +instance subsingleton_prop (p : Prop) : subsingleton p := ⟨λ a b, proof_irrel a b⟩ -attribute [instance] -definition subsingleton_decidable (p : Prop) : subsingleton (decidable p) := +instance subsingleton_decidable (p : Prop) : subsingleton (decidable p) := subsingleton.intro (λ d₁, match d₁ with | (is_true t₁) := (λ d₂, diff --git a/library/init/nat.lean b/library/init/nat.lean index a261dd2351..3fb27a6a44 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -85,8 +85,7 @@ namespace nat | nat_refl : le a -- use nat_refl to avoid overloading le.refl | step : Π {b}, le b → le (succ b) - attribute [instance, priority nat.prio] - definition nat_has_le : has_le ℕ := + instance : has_le ℕ := ⟨nat.le⟩ attribute [refl] @@ -96,8 +95,7 @@ namespace nat attribute [reducible] protected definition lt (n m : ℕ) := succ n ≤ m - attribute [instance, priority nat.prio] - definition nat_has_lt : has_lt ℕ := + instance : has_lt ℕ := ⟨nat.lt⟩ definition pred : ℕ → ℕ @@ -111,12 +109,10 @@ namespace nat protected definition mul (a b : ℕ) : ℕ := nat.rec_on b zero (λ b₁ r, r + a) - attribute [instance, priority nat.prio] - definition nat_has_sub : has_sub ℕ := + instance : has_sub ℕ := ⟨nat.sub⟩ - attribute [instance, priority nat.prio] - definition nat_has_mul : has_mul ℕ := + instance : has_mul ℕ := ⟨nat.mul⟩ attribute [instance, priority nat.prio] @@ -369,7 +365,6 @@ namespace nat | 0 a := a | (succ n) a := f n (repeat n a) - attribute [instance] - protected definition is_inhabited : inhabited ℕ := + instance : inhabited ℕ := ⟨nat.zero⟩ end nat diff --git a/library/init/nat_div.lean b/library/init/nat_div.lean index 2f2e0f3f2b..69ebcca746 100644 --- a/library/init/nat_div.lean +++ b/library/init/nat_div.lean @@ -15,8 +15,7 @@ if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero protected definition div := well_founded.fix lt_wf div.F -attribute[instance] -definition nat_has_divide : has_div nat := +instance : has_div nat := ⟨nat.div⟩ theorem div_def (x y : nat) : div x y = if H : 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := @@ -27,8 +26,7 @@ if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x protected definition mod := well_founded.fix lt_wf mod.F -attribute [instance] -definition nat_has_mod : has_mod nat := +instance : has_mod nat := ⟨nat.mod⟩ theorem mod_def (x y : nat) : mod x y = if H : 0 < y ∧ y ≤ x then mod (x - y) y else x := diff --git a/library/init/num.lean b/library/init/num.lean index 9a9194cb04..79c53da704 100644 --- a/library/init/num.lean +++ b/library/init/num.lean @@ -33,8 +33,7 @@ namespace pos_num pos_num.lt a (succ b) end pos_num -attribute [instance] -definition pos_num_has_mul : has_mul pos_num := +instance : has_mul pos_num := ⟨pos_num.mul⟩ namespace num @@ -50,8 +49,7 @@ namespace num num.rec_on a zero (λ pa, num.rec_on b zero (λ pb, pos (pos_num.mul pa pb))) end num -attribute [instance] -definition num_has_mul : has_mul num := +instance : has_mul num := ⟨num.mul⟩ namespace num @@ -81,6 +79,5 @@ namespace num num.rec_on a zero (λ pa, num.rec_on b a (λ pb, psub pa pb)) end num -attribute [instance] -definition num_has_sub : has_sub num := +instance : has_sub num := ⟨num.sub⟩ diff --git a/library/init/option.lean b/library/init/option.lean index a926493c3e..ccc50fd004 100644 --- a/library/init/option.lean +++ b/library/init/option.lean @@ -9,12 +9,10 @@ open decidable universe variables u v -attribute [instance] -definition option_is_inhabited (A : Type u) : inhabited (option A) := +instance (A : Type u) : inhabited (option A) := ⟨none⟩ -attribute [instance] -definition option_has_decidable_eq {A : Type u} [H : decidable_eq A] : ∀ o₁ o₂ : option A, decidable (o₁ = o₂) +instance {A : Type u} [H : decidable_eq A] : decidable_eq (option A) | none none := is_true rfl | none (some v₂) := is_false (λ H, option.no_confusion H) | (some v₁) none := is_false (λ H, option.no_confusion H) @@ -34,8 +32,7 @@ definition option_bind {A : Type u} {B : Type v} : option A → (A → option B) | none b := none | (some a) b := b a -attribute [instance] -definition option_is_monad : monad option := +instance : monad option := monad.mk @option_fmap @some @option_bind definition option_orelse {A : Type u} : option A → option A → option A @@ -43,8 +40,7 @@ definition option_orelse {A : Type u} : option A → option A → option A | none (some a) := some a | none none := none -attribute [instance] -definition option_is_alternative {A : Type u} : alternative option := +instance {A : Type u} : alternative option := alternative.mk @option_fmap @some (@fapp _ _) @none @option_orelse definition optionT (M : Type (max 1 u) → Type v) [monad M] (A : Type u) : Type v := @@ -74,8 +70,7 @@ definition optionT_return {M : Type (max 1 u) → Type v} [monad M] {A : Type u} show M (option A), from return (some a) -attribute [instance] -definition optionT_is_monad {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : monad (optionT M) := +instance {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : monad (optionT M) := monad.mk (@optionT_fmap M _) (@optionT_return M _) (@optionT_bind M _) definition optionT_orelse {M : Type (max 1 u) → Type v} [monad M] {A : Type u} (a : optionT M A) (b : optionT M A) : optionT M A := @@ -90,11 +85,10 @@ definition optionT_fail {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : show M (option A), from return none -attribute [instance] -definition optionT_is_alternative {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : alternative (optionT M) := +instance {M : Type (max 1 u) → Type v} [monad M] {A : Type u} : alternative (optionT M) := alternative.mk (@optionT_fmap M _) (@optionT_return M _) - (@fapp (optionT M) (@optionT_is_monad M _ A)) + (@fapp (optionT M) (@optionT.monad M _ A)) (@optionT_fail M _) (@optionT_orelse M _) diff --git a/library/init/ordering.lean b/library/init/ordering.lean index e9ed163480..fc9d950231 100644 --- a/library/init/ordering.lean +++ b/library/init/ordering.lean @@ -11,8 +11,7 @@ inductive ordering open ordering -attribute [instance] -definition ordering.has_to_string : has_to_string ordering := +instance : has_to_string ordering := has_to_string.mk (λ s, match s with | ordering.lt := "lt" | ordering.eq := "eq" | ordering.gt := "gt" end) structure [class] has_ordering (A : Type) := @@ -23,8 +22,7 @@ if a < b then ordering.lt else if a = b then ordering.eq else ordering.gt -attribute [instance] -definition nat_has_ordering : has_ordering nat := +instance : has_ordering nat := ⟨nat.cmp⟩ section @@ -40,8 +38,7 @@ definition prod.cmp : A × B → A × B → ordering | ordering.gt := gt end -attribute [instance] -definition prod_has_ordering {A B : Type} [has_ordering A] [has_ordering B] : has_ordering (A × B) := +instance {A B : Type} [has_ordering A] [has_ordering B] : has_ordering (A × B) := ⟨prod.cmp⟩ end @@ -56,8 +53,7 @@ definition sum.cmp : A ⊕ B → A ⊕ B → ordering | (inl a₁) (inr b₂) := lt | (inr b₁) (inl a₂) := gt -attribute [instance] -definition sum_has_ordering {A B : Type} [has_ordering A] [has_ordering B] : has_ordering (A ⊕ B) := +instance {A B : Type} [has_ordering A] [has_ordering B] : has_ordering (A ⊕ B) := ⟨sum.cmp⟩ end @@ -72,7 +68,6 @@ definition option.cmp : option A → option A → ordering | none (some a₂) := lt | none none := eq -attribute [instance] -definition option_has_ordering {A : Type} [has_ordering A] : has_ordering (option A) := +instance {A : Type} [has_ordering A] : has_ordering (option A) := ⟨option.cmp⟩ end diff --git a/library/init/prod.lean b/library/init/prod.lean index 35d4136ceb..f620ea4ea1 100644 --- a/library/init/prod.lean +++ b/library/init/prod.lean @@ -11,12 +11,10 @@ notation `(` h `, ` t:(foldr `, ` (e r, prod.mk e r)) `)` := prod.mk h t universe variables u v -attribute [instance] -protected definition prod.is_inhabited {A : Type u} {B : Type v} [inhabited A] [inhabited B] : inhabited (prod A B) := +instance {A : Type u} {B : Type v} [inhabited A] [inhabited B] : inhabited (prod A B) := ⟨(default A, default B)⟩ -attribute [instance] -protected definition prod.has_decidable_eq {A : Type u} {B : Type v} [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ p₁ p₂ : A × B, decidable (p₁ = p₂) +instance {A : Type u} {B : Type v} [h₁ : decidable_eq A] [h₂ : decidable_eq B] : decidable_eq (A × B) | (a, b) (a', b') := match (h₁ a a') with | (is_true e₁) := diff --git a/library/init/quot.lean b/library/init/quot.lean index 4a53b494f3..4cb6310810 100644 --- a/library/init/quot.lean +++ b/library/init/quot.lean @@ -182,8 +182,7 @@ end quot attribute quot.mk open decidable -attribute [instance] -definition quot.has_decidable_eq {A : Type u} {s : setoid A} [decR : ∀ a b : A, decidable (a ≈ b)] : decidable_eq (quot s) := +instance {A : Type u} {s : setoid A} [decR : ∀ a b : A, decidable (a ≈ b)] : decidable_eq (quot s) := λ q₁ q₂ : quot s, quot.rec_on_subsingleton₂ q₁ q₂ (λ a₁ a₂, diff --git a/library/init/set.lean b/library/init/set.lean index f7851537a7..bbbfae1434 100644 --- a/library/init/set.lean +++ b/library/init/set.lean @@ -33,8 +33,7 @@ p private definition sep (p : A → Prop) (s : set A) : set A := λ a, a ∈ s ∧ p a -attribute [instance] -definition set_is_separable : separable A set := +instance : separable A set := ⟨sep⟩ private definition empty : set A := @@ -43,8 +42,7 @@ private definition empty : set A := private definition insert (a : A) (s : set A) : set A := λ b, b = a ∨ b ∈ s -attribute [instance] -definition set_is_insertable : insertable A set := +instance : insertable A set := ⟨empty, insert⟩ definition union (s₁ s₂ : set A) : set A := @@ -58,8 +56,7 @@ notation s₁ ∩ s₂ := inter s₁ s₂ definition compl (s : set A) : set A := λ a, a ∉ s -attribute [instance] -definition set_has_neg : has_neg (set A) := +instance : has_neg (set A) := ⟨compl⟩ definition diff (s t : set A) : set A := diff --git a/library/init/simplifier.lean b/library/init/simplifier.lean index b445b7ebb4..f486de5a97 100644 --- a/library/init/simplifier.lean +++ b/library/init/simplifier.lean @@ -7,12 +7,10 @@ universe variables u structure [class] is_associative {A : Type u} (op : A → A → A) := (op_assoc : ∀ x y z : A, op (op x y) z = op x (op y z)) -attribute [instance] -definition and_is_associative : is_associative and := +instance : is_associative and := is_associative.mk (λ x y z, propext (@and.assoc x y z)) -attribute [instance] -definition or_is_associative : is_associative or := +instance : is_associative or := is_associative.mk (λ x y z, propext (@or.assoc x y z)) -- Basic congruence theorems over equality (using propext) diff --git a/library/init/state.lean b/library/init/state.lean index 08ed7347c1..a7befcb555 100644 --- a/library/init/state.lean +++ b/library/init/state.lean @@ -25,9 +25,8 @@ attribute [inline] definition state_bind (a : state S A) (b : A → state S B) : state S B := λ s, match (a s) with (a', s') := b a' s' end -attribute [instance] -definition state_is_monad (S : Type) : monad (state S) := -monad.mk (@state_fmap S) (@state_return S) (@state_bind S) +instance (S : Type) : monad (state S) := +⟨@state_fmap S, @state_return S, @state_bind S⟩ end namespace state @@ -64,9 +63,8 @@ section act₂ a new_s end -attribute [instance] -definition stateT_is_monad (S : Type) (M : Type → Type) [monad M] : monad (stateT S M) := -monad.mk (@stateT_fmap S M _) (@stateT_return S M _) (@stateT_bind S M _) +instance (S : Type) (M : Type → Type) [monad M] : monad (stateT S M) := +⟨@stateT_fmap S M _, @stateT_return S M _, @stateT_bind S M _⟩ namespace stateT definition read {S : Type} {M : Type → Type} [monad M] : stateT S M S := diff --git a/library/init/string.lean b/library/init/string.lean index b9b536a732..8da5f1cc62 100644 --- a/library/init/string.lean +++ b/library/init/string.lean @@ -20,8 +20,7 @@ definition concat (a b : string) : string := list.append b a end string -attribute [instance] -definition string.has_append : has_append string := +instance : has_append string := ⟨string.concat⟩ open list diff --git a/library/init/subtype.lean b/library/init/subtype.lean index e9f06dd398..9878a56ee7 100644 --- a/library/init/subtype.lean +++ b/library/init/subtype.lean @@ -29,8 +29,5 @@ end subtype open subtype -variables {A : Type u} {p : A → Prop} - -attribute [instance] -protected definition subtype.is_inhabited {a : A} (h : p a) : inhabited {x // p x} := +instance {A : Type u} {p : A → Prop} {a : A} (h : p a) : inhabited {x // p x} := ⟨⟨a, h⟩⟩ diff --git a/library/init/sum.lean b/library/init/sum.lean index 5bcdc1c424..93e07d188f 100644 --- a/library/init/sum.lean +++ b/library/init/sum.lean @@ -14,10 +14,8 @@ universe variables u v variables {A : Type u} {B : Type v} -attribute [instance] -protected definition is_inhabited_left [h : inhabited A] : inhabited (A ⊕ B) := +instance sum.inhabited_left [h : inhabited A] : inhabited (A ⊕ B) := ⟨sum.inl (default A)⟩ -attribute [instance] -protected definition is_inhabited_right [h : inhabited B] : inhabited (A ⊕ B) := +instance sum.inhabited_right [h : inhabited B] : inhabited (A ⊕ B) := ⟨sum.inr (default B)⟩ diff --git a/library/init/to_string.lean b/library/init/to_string.lean index 7a34e396da..7a118d3006 100644 --- a/library/init/to_string.lean +++ b/library/init/to_string.lean @@ -13,12 +13,10 @@ structure [class] has_to_string (A : Type u) := definition to_string {A : Type u} [has_to_string A] : A → string := has_to_string.to_string -attribute [instance] -definition bool.has_to_string : has_to_string bool := +instance : has_to_string bool := ⟨λ b, cond b "tt" "ff"⟩ -attribute [instance] -definition decidable.has_to_string {p : Prop} : has_to_string (decidable p) := +instance {p : Prop} : has_to_string (decidable p) := -- Remark: type class inference will not consider local instance `b` in the new elaborator ⟨λ b : decidable p, @ite p b _ "tt" "ff"⟩ @@ -31,33 +29,25 @@ definition list.to_string {A : Type u} [has_to_string A] : list A → string | [] := "[]" | (x::xs) := "[" ++ list.to_string_aux tt (x::xs) ++ "]" -attribute [instance] -definition list.has_to_string {A : Type u} [has_to_string A] : has_to_string (list A) := +instance {A : Type u} [has_to_string A] : has_to_string (list A) := ⟨list.to_string⟩ -attribute [instance] -definition unit.has_to_string : has_to_string unit := +instance : has_to_string unit := ⟨λ u, "star"⟩ -attribute [instance] -definition option.has_to_string {A : Type u} [has_to_string A] : has_to_string (option A) := +instance {A : Type u} [has_to_string A] : has_to_string (option A) := ⟨λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")" end⟩ -attribute [instance] -definition sum.has_to_string {A : Type u} {B : Type v} [has_to_string A] [has_to_string B] : has_to_string (A ⊕ B) := +instance {A : Type u} {B : Type v} [has_to_string A] [has_to_string B] : has_to_string (A ⊕ B) := ⟨λ s, match s with | (inl a) := "(inl " ++ to_string a ++ ")" | (inr b) := "(inr " ++ to_string b ++ ")" end⟩ -attribute [instance] -definition prod.has_to_string {A : Type u} {B : Type v} [has_to_string A] [has_to_string B] : has_to_string (A × B) := +instance {A : Type u} {B : Type v} [has_to_string A] [has_to_string B] : has_to_string (A × B) := ⟨λ p, "(" ++ to_string (fst p) ++ ", " ++ to_string (snd p) ++ ")"⟩ -attribute [instance] -definition sigma.has_to_string {A : Type u} {B : A → Type v} [has_to_string A] [s : ∀ x, has_to_string (B x)] - : has_to_string (sigma B) := +instance {A : Type u} {B : A → Type v} [has_to_string A] [s : ∀ x, has_to_string (B x)] : has_to_string (sigma B) := ⟨λ p, "⟨" ++ to_string (fst p) ++ ", " ++ to_string (snd p) ++ "⟩"⟩ -attribute [instance] -definition subtype.has_to_string {A : Type u} {P : A → Prop} [has_to_string A] : has_to_string (subtype P) := +instance {A : Type u} {P : A → Prop} [has_to_string A] : has_to_string (subtype P) := ⟨λ s, to_string (elt_of s)⟩ definition char.quote_core (c : char) : string := @@ -67,8 +57,7 @@ else if c = '\"' then "\\\"" else if c = '\'' then "\\\'" else c::nil -attribute [instance] -definition char.has_to_sting : has_to_string char := +instance : has_to_string char := ⟨λ c, "'" ++ char.quote_core c ++ "'"⟩ definition string.quote_aux : string → string @@ -79,8 +68,7 @@ definition string.quote : string → string | [] := "\"\"" | (x::xs) := "\"" ++ string.quote_aux (x::xs) ++ "\"" -attribute [instance] -definition string.has_to_string : has_to_string string := +instance : has_to_string string := ⟨string.quote⟩ /- Remark: the code generator replaces this definition with one that display natural numbers in decimal notation -/ @@ -88,14 +76,11 @@ definition nat.to_string : nat → string | 0 := "zero" | (succ a) := "(succ " ++ nat.to_string a ++ ")" -attribute [instance] -definition nat.has_to_string : has_to_string nat := +instance : has_to_string nat := ⟨nat.to_string⟩ -attribute [instance] -definition fin.has_to_string (n : nat) : has_to_string (fin n) := +instance (n : nat) : has_to_string (fin n) := ⟨λ f, to_string (fin.val f)⟩ -attribute [instance] -definition unsigned.has_to_string : has_to_string unsigned := +instance : has_to_string unsigned := ⟨λ n, to_string (fin.val n)⟩ diff --git a/library/init/unit.lean b/library/init/unit.lean index 8a69ec30ab..d12c5bbe2e 100644 --- a/library/init/unit.lean +++ b/library/init/unit.lean @@ -12,10 +12,8 @@ unit.rec_on a (unit.rec_on b rfl) theorem unit_eq_unit (a : unit) : a = () := unit_eq a () -attribute [instance] -definition unit_subsingleton : subsingleton unit := +instance : subsingleton unit := subsingleton.intro unit_eq -attribute [instance] -definition unit_is_inhabited : inhabited unit := +instance : inhabited unit := ⟨()⟩ diff --git a/library/init/unsigned.lean b/library/init/unsigned.lean index 6f84808582..3b527c8d5c 100644 --- a/library/init/unsigned.lean +++ b/library/init/unsigned.lean @@ -24,7 +24,6 @@ definition to_nat (c : unsigned) : nat := fin.val c end unsigned -attribute [instance] -definition unsigned.has_decidable_eq : decidable_eq unsigned := -have decidable_eq (fin unsigned_sz), from fin.has_decidable_eq _, +instance : decidable_eq unsigned := +have decidable_eq (fin unsigned_sz), from fin.decidable_eq _, this diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index b83c82e323..517fe90f51 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -131,7 +131,7 @@ ;; attributes after definitions (,(rx word-start (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary" - "hypothesis" "definition" "meta_definition" "instance" "constant" "meta_constant")) + "hypothesis" "definition" "meta_definition" "constant" "meta_constant")) word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace))) (zero-or-more whitespace) @@ -141,7 +141,7 @@ (2 'font-lock-doc-face) (4 'font-lock-function-name-face)) (,(rx word-start (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary" - "hypothesis" "definition" "meta_definition" "instance" "constant" "meta_constant")) + "hypothesis" "definition" "meta_definition" "constant" "meta_constant")) word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace))) (zero-or-more whitespace) @@ -149,7 +149,7 @@ (2 'font-lock-doc-face) (3 'font-lock-function-name-face)) (,(rx word-start (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary" - "hypothesis" "definition" "meta_definition" "instance" "constant" "meta_constant")) + "hypothesis" "definition" "meta_definition" "constant" "meta_constant")) word-end (zero-or-more whitespace) (group (zero-or-more "{" (zero-or-more (not (any "}"))) "}" (zero-or-more whitespace))) (zero-or-more whitespace) @@ -180,7 +180,7 @@ ;; universe/inductive/theorem... "names" (without attributes) (,(rx word-start (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary" - "hypothesis" "definition" "meta_definition" "instance" "constant" "meta_constant")) + "hypothesis" "definition" "meta_definition" "constant" "meta_constant")) word-end (zero-or-more whitespace) (group (zero-or-more (not (any " \t\n\r{(["))))) diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 39d13e4212..dcabf31199 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -81,10 +81,9 @@ void decl_attributes::parse(parser & p) { } } -void decl_attributes::add_attribute(environment const & env, name const & attr_name) { - if (!is_attribute(env, attr_name)) - throw exception(sstream() << "unknown attribute [" << attr_name << "]"); - auto const & attr = get_attribute(env, attr_name); +void decl_attributes::set_instance_cmd(environment const & env) { + auto const & attr = get_attribute(env, "instance"); + m_instance_cmd = true; m_entries = cons({&attr, get_default_attr_data()}, m_entries); } diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h index c36f779d72..61ba51641f 100644 --- a/src/frontends/lean/decl_attributes.h +++ b/src/frontends/lean/decl_attributes.h @@ -21,11 +21,13 @@ public: private: bool m_persistent; bool m_parsing_only; + bool m_instance_cmd; list m_entries; optional m_prio; public: - decl_attributes(bool persistent = true): m_persistent(persistent), m_parsing_only(false) {} - void add_attribute(environment const & env, name const & attr_name); + decl_attributes(bool persistent = true): m_persistent(persistent), m_parsing_only(false), m_instance_cmd(false) {} + void set_instance_cmd(environment const & env); + bool is_instance_cmd() const { return m_instance_cmd; } void parse(parser & p); environment apply(environment env, io_state const & ios, name const & d) const; list const & get_entries() const { return m_entries; } diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 42b44ca3bf..7f82441ba9 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -571,8 +571,8 @@ static environment reveal_cmd(parser & p) { static environment instance_cmd(parser & p) { bool persistent = true; - decl_attributes attributes(true); - attributes.add_attribute(p.env(), "instance"); + decl_attributes attributes(persistent); + attributes.set_instance_cmd(p.env()); bool is_private = false; bool is_protected = true; bool is_noncomputable = false; return definition_cmd_core(p, def_cmd_kind::Definition, is_private, is_protected, is_noncomputable, attributes); } diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index e22069912d..30a5ceb8d4 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -55,14 +55,18 @@ bool parse_univ_params(parser & p, buffer & lp_names) { } } -expr parse_single_header(parser & p, buffer & lp_names, buffer & params, bool is_example) { +expr parse_single_header(parser & p, buffer & lp_names, buffer & params, + bool is_example, bool is_instance) { + lean_assert(!is_example || !is_instance); auto c_pos = p.pos(); name c_name; if (is_example) { c_name = name("this"); } else { - parse_univ_params(p, lp_names); - c_name = p.check_decl_id_next("invalid declaration, identifier expected"); + if (!is_instance) + parse_univ_params(p, lp_names); + if (!is_instance || p.curr_is_identifier()) + c_name = p.check_decl_id_next("invalid declaration, identifier expected"); } declaration_name_scope scope(c_name); p.parse_optional_binders(params); @@ -75,8 +79,23 @@ expr parse_single_header(parser & p, buffer & lp_names, buffer & par } else { type = p.save_pos(mk_expr_placeholder(), c_pos); } - expr c = p.save_pos(mk_local(c_name, type), c_pos); - return c; + + if (is_instance && c_name.is_anonymous()) { + /* Try to synthesize name */ + expr it = type; + while (is_pi(it)) it = binding_body(it); + expr const & C = get_app_fn(it); + name ns = get_namespace(p.env()); + if (is_constant(C) && !ns.is_anonymous()) { + c_name = const_name(C); + } else if (is_constant(C) && is_app(it) && is_constant(get_app_fn(app_arg(it)))) { + c_name = const_name(get_app_fn(app_arg(it))) + const_name(C); + } else { + throw parser_error("failed to synthesize instance name, name should be provided explicitly", c_pos); + } + } + lean_assert(!c_name.is_anonymous()); + return p.save_pos(mk_local(c_name, type), c_pos); } void parse_mutual_header(parser & p, buffer & lp_names, buffer & cs, buffer & params) { diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h index b2bc9b1414..2ca2ddbc79 100644 --- a/src/frontends/lean/decl_util.h +++ b/src/frontends/lean/decl_util.h @@ -33,7 +33,8 @@ bool parse_old_univ_params(parser & p, buffer & lp_names); Both lp_names and params are added to the parser scope. \remark Caller is responsible for using: parser::local_scope scope2(p, env); */ -expr parse_single_header(parser & p, buffer & lp_names, buffer & params, bool is_example = false); +expr parse_single_header(parser & p, buffer & lp_names, buffer & params, + bool is_example = false, bool is_instance = false); /** \brief Parse the header of a mutually recursive declaration. It has the form {u_1 ... u_k} id_1, ... id_n (params) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 3677e31888..96f88e67c0 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -152,10 +152,11 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, bool is_pr return p.env(); } -static expr_pair parse_definition(parser & p, buffer & lp_names, buffer & params, bool is_example) { +static expr_pair parse_definition(parser & p, buffer & lp_names, buffer & params, + bool is_example, bool is_instance) { parser::local_scope scope1(p); auto header_pos = p.pos(); - expr fn = parse_single_header(p, lp_names, params, is_example); + expr fn = parse_single_header(p, lp_names, params, is_example, is_instance); declaration_name_scope scope2(local_pp_name(fn)); expr val; if (p.curr_is_token(get_assign_tk())) { @@ -379,7 +380,9 @@ environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private, expr fn, val; auto header_pos = p.pos(); declaration_info_scope scope(p, is_private, is_noncomputable, kind); - std::tie(fn, val) = parse_definition(p, lp_names, params, kind == def_cmd_kind::Example); + bool is_example = (kind == def_cmd_kind::Example); + bool is_instance = attrs.is_instance_cmd(); + std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance); elaborator elab(p.env(), p.get_options(), metavar_context(), local_context()); buffer new_params; elaborate_params(elab, params, new_params); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index ac9ddeec72..c778bfdff4 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -481,16 +481,16 @@ void initialize_constants() { g_insert = new name{"insert"}; g_int = new name{"int"}; g_int_of_nat = new name{"int", "of_nat"}; - g_int_has_zero = new name{"int_has_zero"}; - g_int_has_one = new name{"int_has_one"}; - g_int_has_add = new name{"int_has_add"}; - g_int_has_mul = new name{"int_has_mul"}; - g_int_has_sub = new name{"int_has_sub"}; - g_int_has_div = new name{"int_has_div"}; - g_int_has_le = new name{"int_has_le"}; - g_int_has_lt = new name{"int_has_lt"}; - g_int_has_neg = new name{"int_has_neg"}; - g_int_has_mod = new name{"int_has_mod"}; + g_int_has_zero = new name{"int", "has_zero"}; + g_int_has_one = new name{"int", "has_one"}; + g_int_has_add = new name{"int", "has_add"}; + g_int_has_mul = new name{"int", "has_mul"}; + g_int_has_sub = new name{"int", "has_sub"}; + g_int_has_div = new name{"int", "has_div"}; + g_int_has_le = new name{"int", "has_le"}; + g_int_has_lt = new name{"int", "has_lt"}; + g_int_has_neg = new name{"int", "has_neg"}; + g_int_has_mod = new name{"int", "has_mod"}; g_int_decidable_linear_ordered_comm_group = new name{"int_decidable_linear_ordered_comm_group"}; g_IO = new name{"IO"}; g_is_associative = new name{"is_associative"}; @@ -536,15 +536,15 @@ void initialize_constants() { g_nat_of_num = new name{"nat", "of_num"}; g_nat_succ = new name{"nat", "succ"}; g_nat_zero = new name{"nat", "zero"}; - g_nat_has_zero = new name{"nat_has_zero"}; - g_nat_has_one = new name{"nat_has_one"}; - g_nat_has_add = new name{"nat_has_add"}; - g_nat_has_mul = new name{"nat_has_mul"}; - g_nat_has_div = new name{"nat_has_div"}; - g_nat_has_sub = new name{"nat_has_sub"}; - g_nat_has_neg = new name{"nat_has_neg"}; - g_nat_has_lt = new name{"nat_has_lt"}; - g_nat_has_le = new name{"nat_has_le"}; + g_nat_has_zero = new name{"nat", "has_zero"}; + g_nat_has_one = new name{"nat", "has_one"}; + g_nat_has_add = new name{"nat", "has_add"}; + g_nat_has_mul = new name{"nat", "has_mul"}; + g_nat_has_div = new name{"nat", "has_div"}; + g_nat_has_sub = new name{"nat", "has_sub"}; + g_nat_has_neg = new name{"nat", "has_neg"}; + g_nat_has_lt = new name{"nat", "has_lt"}; + g_nat_has_le = new name{"nat", "has_le"}; g_nat_add = new name{"nat", "add"}; g_nat_no_confusion = new name{"nat", "no_confusion"}; g_nat_cases_on = new name{"nat", "cases_on"}; @@ -640,15 +640,15 @@ void initialize_constants() { g_rat_of_num = new name{"rat", "of_num"}; g_rat_of_int = new name{"rat", "of_int"}; g_real = new name{"real"}; - g_real_has_zero = new name{"real_has_zero"}; - g_real_has_one = new name{"real_has_one"}; - g_real_has_add = new name{"real_has_add"}; - g_real_has_mul = new name{"real_has_mul"}; - g_real_has_sub = new name{"real_has_sub"}; - g_real_has_div = new name{"real_has_div"}; - g_real_has_le = new name{"real_has_le"}; - g_real_has_lt = new name{"real_has_lt"}; - g_real_has_neg = new name{"real_has_neg"}; + g_real_has_zero = new name{"real", "has_zero"}; + g_real_has_one = new name{"real", "has_one"}; + g_real_has_add = new name{"real", "has_add"}; + g_real_has_mul = new name{"real", "has_mul"}; + g_real_has_sub = new name{"real", "has_sub"}; + g_real_has_div = new name{"real", "has_div"}; + g_real_has_le = new name{"real", "has_le"}; + g_real_has_lt = new name{"real", "has_lt"}; + g_real_has_neg = new name{"real", "has_neg"}; g_real_is_int = new name{"real", "is_int"}; g_real_of_rat = new name{"real", "of_rat"}; g_real_of_int = new name{"real", "of_int"}; diff --git a/src/library/constants.txt b/src/library/constants.txt index 4408bf1e4c..1dcab69f18 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -118,16 +118,16 @@ implies.resolve insert int int.of_nat -int_has_zero -int_has_one -int_has_add -int_has_mul -int_has_sub -int_has_div -int_has_le -int_has_lt -int_has_neg -int_has_mod +int.has_zero +int.has_one +int.has_add +int.has_mul +int.has_sub +int.has_div +int.has_le +int.has_lt +int.has_neg +int.has_mod int_decidable_linear_ordered_comm_group IO is_associative @@ -173,15 +173,15 @@ nat nat.of_num nat.succ nat.zero -nat_has_zero -nat_has_one -nat_has_add -nat_has_mul -nat_has_div -nat_has_sub -nat_has_neg -nat_has_lt -nat_has_le +nat.has_zero +nat.has_one +nat.has_add +nat.has_mul +nat.has_div +nat.has_sub +nat.has_neg +nat.has_lt +nat.has_le nat.add nat.no_confusion nat.cases_on @@ -277,15 +277,15 @@ rat.divide rat.of_num rat.of_int real -real_has_zero -real_has_one -real_has_add -real_has_mul -real_has_sub -real_has_div -real_has_le -real_has_lt -real_has_neg +real.has_zero +real.has_one +real.has_add +real.has_mul +real.has_sub +real.has_div +real.has_le +real.has_lt +real.has_neg real.is_int real.of_rat real.of_int diff --git a/tests/lean/584a.lean.expected.out b/tests/lean/584a.lean.expected.out index c8171e3c71..c8a10c4777 100644 --- a/tests/lean/584a.lean.expected.out +++ b/tests/lean/584a.lean.expected.out @@ -1,5 +1,5 @@ foo : Π (A : Type u_1) [H : inhabited A], A → A foo' : Π {A : Type u_1} [H : inhabited A] {x : A}, A foo ℕ 10 : ℕ -definition test : ∀ {A : Type u} [H : inhabited A], @foo' ℕ nat.is_inhabited (5 + 5) = 10 := -λ {A : Type u} [H : inhabited A], @rfl ℕ (@foo' ℕ nat.is_inhabited (5 + 5)) +definition test : ∀ {A : Type u} [H : inhabited A], @foo' ℕ nat.inhabited (5 + 5) = 10 := +λ {A : Type u} [H : inhabited A], @rfl ℕ (@foo' ℕ nat.inhabited (5 + 5)) diff --git a/tests/lean/attributes.lean b/tests/lean/attributes.lean index a221f0e52a..329e62201d 100644 --- a/tests/lean/attributes.lean +++ b/tests/lean/attributes.lean @@ -6,4 +6,4 @@ local attribute [-reducible] foo -- use [semireducible] instead -- -local attribute [-instance] nat_has_one +local attribute [-instance] nat.has_one diff --git a/tests/lean/coe4.lean.expected.out b/tests/lean/coe4.lean.expected.out index 1dc601f7e6..486812811e 100644 --- a/tests/lean/coe4.lean.expected.out +++ b/tests/lean/coe4.lean.expected.out @@ -1,5 +1,5 @@ ⇑f 0 1 : ℕ f 0 1 : ℕ ⇑f 0 1 : ℕ -@coe_fn.{1 1} (Functor.{1} nat) (coe_functor_to_fn.{1} nat) f (@zero.{1} nat nat_has_zero) (@one.{1} nat nat_has_one) : +@coe_fn.{1 1} (Functor.{1} nat) (coe_functor_to_fn.{1} nat) f (@zero.{1} nat nat.has_zero) (@one.{1} nat nat.has_one) : nat diff --git a/tests/lean/defeq_simp1.lean b/tests/lean/defeq_simp1.lean index 432fc79632..4ccd279735 100644 --- a/tests/lean/defeq_simp1.lean +++ b/tests/lean/defeq_simp1.lean @@ -7,14 +7,14 @@ set_option pp.all true open tactic -example (a b : nat) (H : @add nat (id (id nat_has_add)) a b = @add nat nat_has_add2 a b) : true := +example (a b : nat) (H : @add nat (id (id nat.has_add)) a b = @add nat nat_has_add2 a b) : true := by do get_local `H >>= infer_type >>= defeq_simp >>= trace, constructor constant x1 : nat -- update the environment to force defeq_canonize cache to be reset -example (a b : nat) (H : (λ x : nat, @add nat (id (id nat_has_add)) a b) = (λ x : nat, @add nat nat_has_add2 a x)) : true := +example (a b : nat) (H : (λ x : nat, @add nat (id (id nat.has_add)) a b) = (λ x : nat, @add nat nat_has_add2 a x)) : true := by do get_local `H >>= infer_type >>= defeq_simp >>= trace, constructor diff --git a/tests/lean/elab2.lean.expected.out b/tests/lean/elab2.lean.expected.out index 7bee78eeb1..91499dcff9 100644 --- a/tests/lean/elab2.lean.expected.out +++ b/tests/lean/elab2.lean.expected.out @@ -1,4 +1,4 @@ -@foo.{1 1} nat nat nat_has_add (@zero.{1} nat nat_has_zero) (@one.{1} nat nat_has_one) : nat +@foo.{1 1} nat nat nat.has_add (@zero.{1} nat nat.has_zero) (@one.{1} nat nat.has_one) : nat elab2.lean:13:6: error: type mismatch at application @bla.{1 ?l_1} nat ?m_2 nat.zero bool.tt term @@ -7,4 +7,4 @@ has type bool but is expected to have type nat -@bla.{1 1} nat bool (@zero.{1} nat nat_has_zero) (@zero.{1} nat nat_has_zero) bool.tt : nat +@bla.{1 1} nat bool (@zero.{1} nat nat.has_zero) (@zero.{1} nat nat.has_zero) bool.tt : nat diff --git a/tests/lean/elab7.lean.expected.out b/tests/lean/elab7.lean.expected.out index fae622aa24..152a545984 100644 --- a/tests/lean/elab7.lean.expected.out +++ b/tests/lean/elab7.lean.expected.out @@ -1,5 +1,5 @@ -λ (x : nat), @add.{1} nat nat_has_add x (@one.{1} nat nat_has_one) : nat → nat -λ (x y : nat), @add.{1} nat nat_has_add x y : nat → nat → nat -λ (x y : nat), @add.{1} nat nat_has_add (@add.{1} nat nat_has_add x y) (@one.{1} nat nat_has_one) : nat → nat → nat -λ (x : nat), @list.cons.{1} nat (@add.{1} nat nat_has_add x (@one.{1} nat nat_has_one)) (@list.nil.{1} nat) : +λ (x : nat), @add.{1} nat nat.has_add x (@one.{1} nat nat.has_one) : nat → nat +λ (x y : nat), @add.{1} nat nat.has_add x y : nat → nat → nat +λ (x y : nat), @add.{1} nat nat.has_add (@add.{1} nat nat.has_add x y) (@one.{1} nat nat.has_one) : nat → nat → nat +λ (x : nat), @list.cons.{1} nat (@add.{1} nat nat.has_add x (@one.{1} nat nat.has_one)) (@list.nil.{1} nat) : nat → list.{1} nat diff --git a/tests/lean/elab9.lean.expected.out b/tests/lean/elab9.lean.expected.out index 26ebba2870..2135696e95 100644 --- a/tests/lean/elab9.lean.expected.out +++ b/tests/lean/elab9.lean.expected.out @@ -4,5 +4,5 @@ Π (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_zero A] (a : A), @eq A (@add A _inst_1 a (@zero A _inst_2)) a → Π [_inst_3 : has_add A], @eq A a (@add A _inst_3 (@zero A _inst_2) (@zero A _inst_2)) → A -λ (a b : nat) (H : @gt nat nat.nat_has_lt a b) [_inst_1 : has_lt nat], @lt nat _inst_1 a b : - Π (a b : nat), @gt nat nat.nat_has_lt a b → Π [_inst_1 : has_lt nat], Prop +λ (a b : nat) (H : @gt nat nat.has_lt a b) [_inst_1 : has_lt nat], @lt nat _inst_1 a b : + Π (a b : nat), @gt nat nat.has_lt a b → Π [_inst_1 : has_lt nat], Prop diff --git a/tests/lean/eta_tac.lean.expected.out b/tests/lean/eta_tac.lean.expected.out index a1e65920a3..bcf00aa6db 100644 --- a/tests/lean/eta_tac.lean.expected.out +++ b/tests/lean/eta_tac.lean.expected.out @@ -1,4 +1,4 @@ λ {A : Type ?} [_inst_1 : has_add A] (a a_1 : A), @add A _inst_1 a a_1 λ (a : nat), nat.succ a -λ (a_1 : nat), @add nat nat_has_add a a_1 -λ (x a : nat), @add nat nat_has_add x a +λ (a_1 : nat), @add nat nat.has_add a a_1 +λ (x a : nat), @add nat nat.has_add x a diff --git a/tests/lean/pp_all.lean.expected.out b/tests/lean/pp_all.lean.expected.out index 0935a7d5a2..1991b6fb61 100644 --- a/tests/lean/pp_all.lean.expected.out +++ b/tests/lean/pp_all.lean.expected.out @@ -1,5 +1,5 @@ a + of_num b = 10 : Prop -@eq.{1} nat (@add.{1} nat nat_has_add ((λ (x : nat), x) a) (nat.of_num b)) - (@bit0.{1} nat nat_has_add - (@bit1.{1} nat nat_has_one nat_has_add (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one)))) : +@eq.{1} nat (@add.{1} nat nat.has_add ((λ (x : nat), x) a) (nat.of_num b)) + (@bit0.{1} nat nat.has_add + (@bit1.{1} nat nat.has_one nat.has_add (@bit0.{1} nat nat.has_add (@one.{1} nat nat.has_one)))) : Prop diff --git a/tests/lean/pp_all2.lean.expected.out b/tests/lean/pp_all2.lean.expected.out index f7ed80d313..510a3c261f 100644 --- a/tests/lean/pp_all2.lean.expected.out +++ b/tests/lean/pp_all2.lean.expected.out @@ -1 +1 @@ -@add nat nat_has_add 10 3 : nat +@add nat nat.has_add 10 3 : nat diff --git a/tests/lean/qexpr1.lean.expected.out b/tests/lean/qexpr1.lean.expected.out index 6f362546c9..e9c4cf7394 100644 --- a/tests/lean/qexpr1.lean.expected.out +++ b/tests/lean/qexpr1.lean.expected.out @@ -1,4 +1,4 @@ -@add.{1} nat nat_has_add a b +@add.{1} nat nat.has_add a b nat -@add.{1} nat nat_has_add (nat.succ a) b +@add.{1} nat nat.has_add (nat.succ a) b nat diff --git a/tests/lean/qexpr2.lean.expected.out b/tests/lean/qexpr2.lean.expected.out index 044b02b29d..9f97ac6e2b 100644 --- a/tests/lean/qexpr2.lean.expected.out +++ b/tests/lean/qexpr2.lean.expected.out @@ -1,4 +1,4 @@ -@add.{1} nat nat_has_add ?m_1 b +@add.{1} nat nat.has_add ?m_1 b nat ------ after instantiate_mvars -@add.{1} nat nat_has_add c b +@add.{1} nat nat.has_add c b diff --git a/tests/lean/run/968.lean b/tests/lean/run/968.lean index ff13eae6ee..90572184ff 100644 --- a/tests/lean/run/968.lean +++ b/tests/lean/run/968.lean @@ -2,14 +2,14 @@ variables (A : Type) [inhabited A] definition f (a : A) : A := a -check @f nat nat.is_inhabited +check @f nat nat.inhabited structure foo := (a : A) -check @foo nat nat.is_inhabited +check @foo nat nat.inhabited inductive bla | mk : A → bla -check @bla nat nat.is_inhabited +check @bla nat nat.inhabited diff --git a/tests/lean/run/stateT1.lean b/tests/lean/run/stateT1.lean index f33b046f6c..fa1831a311 100644 --- a/tests/lean/run/stateT1.lean +++ b/tests/lean/run/stateT1.lean @@ -1,9 +1,8 @@ - meta_definition mytactic (A : Type) := stateT (list nat) tactic A attribute [instance] meta_definition mytactic_is_monad : monad mytactic := -@stateT_is_monad _ _ _ +@stateT.monad _ _ _ meta_definition read_lst : mytactic (list nat) := stateT.read diff --git a/tests/lean/set_opt_tac.lean.expected.out b/tests/lean/set_opt_tac.lean.expected.out index 9ddb543d53..c3a77a1b30 100644 --- a/tests/lean/set_opt_tac.lean.expected.out +++ b/tests/lean/set_opt_tac.lean.expected.out @@ -1,5 +1,5 @@ a + b = 0 after pp.all true -@eq.{1} nat (@add.{1} nat nat_has_add a b) (@zero.{1} nat nat_has_zero) +@eq.{1} nat (@add.{1} nat nat.has_add a b) (@zero.{1} nat nat.has_zero) set_bool_option tactic does not affect other commands 0 + 1 : ℕ diff --git a/tests/lean/type_class_bug.lean.expected.out b/tests/lean/type_class_bug.lean.expected.out index 66757ef628..e63f95f6c7 100644 --- a/tests/lean/type_class_bug.lean.expected.out +++ b/tests/lean/type_class_bug.lean.expected.out @@ -1,14 +1,14 @@ -@monad.bind.{1 1} list.{1} list_is_monad.{1} nat nat (@list.cons.{1} nat (@one.{1} nat nat_has_one) (@list.nil.{1} nat)) - (λ (a : nat), @return.{1 1} list.{1} list_is_monad.{1} nat a) : +@monad.bind.{1 1} list.{1} list.monad.{1} nat nat (@list.cons.{1} nat (@one.{1} nat nat.has_one) (@list.nil.{1} nat)) + (λ (a : nat), @return.{1 1} list.{1} list.monad.{1} nat a) : list.{1} nat -@monad.bind.{1 1} list.{1} list_is_monad.{1} nat (prod.{1 1} nat nat) - (@list.cons.{1} nat (@one.{1} nat nat_has_one) - (@list.cons.{1} nat (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one)) - (@list.cons.{1} nat (@bit1.{1} nat nat_has_one nat_has_add (@one.{1} nat nat_has_one)) (@list.nil.{1} nat)))) +@monad.bind.{1 1} list.{1} list.monad.{1} nat (prod.{1 1} nat nat) + (@list.cons.{1} nat (@one.{1} nat nat.has_one) + (@list.cons.{1} nat (@bit0.{1} nat nat.has_add (@one.{1} nat nat.has_one)) + (@list.cons.{1} nat (@bit1.{1} nat nat.has_one nat.has_add (@one.{1} nat nat.has_one)) (@list.nil.{1} nat)))) (λ (a : nat), - @monad.bind.{1 1} list.{1} list_is_monad.{1} nat (prod.{1 1} nat nat) - (@list.cons.{1} nat (@bit1.{1} nat nat_has_one nat_has_add (@one.{1} nat nat_has_one)) - (@list.cons.{1} nat (@bit0.{1} nat nat_has_add (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one))) + @monad.bind.{1 1} list.{1} list.monad.{1} nat (prod.{1 1} nat nat) + (@list.cons.{1} nat (@bit1.{1} nat nat.has_one nat.has_add (@one.{1} nat nat.has_one)) + (@list.cons.{1} nat (@bit0.{1} nat nat.has_add (@bit0.{1} nat nat.has_add (@one.{1} nat nat.has_one))) (@list.nil.{1} nat))) - (λ (b : nat), @return.{1 1} list.{1} list_is_monad.{1} (prod.{1 1} nat nat) (@prod.mk.{1 1} nat nat a b))) : + (λ (b : nat), @return.{1 1} list.{1} list.monad.{1} (prod.{1 1} nat nat) (@prod.mk.{1 1} nat nat a b))) : list.{1} (prod.{1 1} nat nat)