feat(frontends/lean): anonymous instances
The instance name is synthesized automatically.
This commit is contained in:
Leonardo de Moura
parent
6bfd4eb9cf
commit
f00e6c0a96
49 changed files with 270 additions and 371 deletions
|
|
@ -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'⟩
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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₁)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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₂,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
|
|
|||
|
|
@ -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 _)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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₁) :=
|
||||
|
|
|
|||
|
|
@ -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₂,
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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⟩⟩
|
||||
|
|
|
|||
|
|
@ -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)⟩
|
||||
|
|
|
|||
|
|
@ -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)⟩
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
⟨()⟩
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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{([")))))
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -21,11 +21,13 @@ public:
|
|||
private:
|
||||
bool m_persistent;
|
||||
bool m_parsing_only;
|
||||
bool m_instance_cmd;
|
||||
list<entry> m_entries;
|
||||
optional<unsigned> 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<entry> const & get_entries() const { return m_entries; }
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -55,14 +55,18 @@ bool parse_univ_params(parser & p, buffer<name> & lp_names) {
|
|||
}
|
||||
}
|
||||
|
||||
expr parse_single_header(parser & p, buffer<name> & lp_names, buffer<expr> & params, bool is_example) {
|
||||
expr parse_single_header(parser & p, buffer<name> & lp_names, buffer<expr> & 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<name> & lp_names, buffer<expr> & 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<name> & lp_names, buffer<expr> & cs, buffer<expr> & params) {
|
||||
|
|
|
|||
|
|
@ -33,7 +33,8 @@ bool parse_old_univ_params(parser & p, buffer<name> & 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<name> & lp_names, buffer<expr> & params, bool is_example = false);
|
||||
expr parse_single_header(parser & p, buffer<name> & lp_names, buffer<expr> & 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)
|
||||
|
|
|
|||
|
|
@ -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<name> & lp_names, buffer<expr> & params, bool is_example) {
|
||||
static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & 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<expr> new_params;
|
||||
elaborate_params(elab, params, new_params);
|
||||
|
|
|
|||
|
|
@ -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"};
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -6,4 +6,4 @@ local attribute [-reducible] foo -- use [semireducible] instead
|
|||
|
||||
--
|
||||
|
||||
local attribute [-instance] nat_has_one
|
||||
local attribute [-instance] nat.has_one
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
@add nat nat_has_add 10 3 : nat
|
||||
@add nat nat.has_add 10 3 : nat
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 : ℕ
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue