diff --git a/library/data/buffer/parser.lean b/library/data/buffer/parser.lean index 543593b043..24cd7e87ab 100644 --- a/library/data/buffer/parser.lean +++ b/library/data/buffer/parser.lean @@ -77,9 +77,9 @@ protected def orelse (p q : parser α) : parser α := end instance : alternative parser := -{ parser.monad_fail with - failure := @parser.failure, - orelse := @parser.orelse } +{ failure := @parser.failure, + orelse := @parser.orelse, + ..parser.monad_fail } instance : inhabited (parser α) := ⟨parser.failure⟩ diff --git a/library/init/algebra/field.lean b/library/init/algebra/field.lean index efa486062f..716775eacb 100644 --- a/library/init/algebra/field.lean +++ b/library/init/algebra/field.lean @@ -338,8 +338,8 @@ decidable.by_cases or.inr (by rw [← one_mul b, ← inv_mul_cancel this, mul_assoc, h, mul_zero])) instance discrete_field.to_integral_domain [s : discrete_field α] : integral_domain α := -{s with - eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero} +{ eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero, + ..s } lemma inv_zero : 0⁻¹ = (0:α) := discrete_field.inv_zero α diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean index ed86cdd0b1..6717661ed5 100644 --- a/library/init/algebra/group.lean +++ b/library/init/algebra/group.lean @@ -112,10 +112,10 @@ have a * b * b⁻¹ = a, by simp, begin simp [h] at this, rw this end instance group.to_left_cancel_semigroup [s : group α] : left_cancel_semigroup α := -{ s with mul_left_cancel := @group.mul_left_cancel α s } +{ mul_left_cancel := @group.mul_left_cancel α s, ..s } instance group.to_right_cancel_semigroup [s : group α] : right_cancel_semigroup α := -{ s with mul_right_cancel := @group.mul_right_cancel α s } +{ mul_right_cancel := @group.mul_right_cancel α s, ..s } lemma mul_inv_cancel_left [group α] (a b : α) : a * (a⁻¹ * b) = b := by rw [← mul_assoc, mul_right_inv, one_mul] diff --git a/library/init/algebra/ordered_field.lean b/library/init/algebra/ordered_field.lean index 7b6c69beff..aee02b3aad 100644 --- a/library/init/algebra/ordered_field.lean +++ b/library/init/algebra/ordered_field.lean @@ -374,8 +374,8 @@ section discrete_linear_ordered_field variables {α : Type u} instance discrete_linear_ordered_field.to_discrete_field [s : discrete_linear_ordered_field α] : discrete_field α := -{s with - has_decidable_eq := @decidable_linear_ordered_comm_ring.decidable_eq α (@discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring α s) } +{ has_decidable_eq := @decidable_linear_ordered_comm_ring.decidable_eq α (@discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring α s), + ..s } variables [discrete_linear_ordered_field α] diff --git a/library/init/algebra/ordered_group.lean b/library/init/algebra/ordered_group.lean index 7f71d40289..8e5e3184ce 100644 --- a/library/init/algebra/ordered_group.lean +++ b/library/init/algebra/ordered_group.lean @@ -201,10 +201,10 @@ begin simp [neg_add_cancel_left] at this, assumption end end ordered_comm_group instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u) [s : ordered_comm_group α] : ordered_cancel_comm_monoid α := -{ s with - add_left_cancel := @add_left_cancel α _, +{ add_left_cancel := @add_left_cancel α _, add_right_cancel := @add_right_cancel α _, - le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left α _ } + le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left α _, + ..s } section ordered_comm_group variables {α : Type u} [ordered_comm_group α] @@ -614,7 +614,7 @@ class decidable_linear_ordered_comm_group (α : Type u) instance decidable_linear_ordered_comm_group.to_ordered_comm_group (α : Type u) [s : decidable_linear_ordered_comm_group α] : ordered_comm_group α := -{ s with add := s.add } +{ add := s.add, ..s } class decidable_linear_ordered_cancel_comm_monoid (α : Type u) extends ordered_cancel_comm_monoid α, decidable_linear_order α diff --git a/library/init/algebra/ordered_ring.lean b/library/init/algebra/ordered_ring.lean index a0751cfd09..8d5de60171 100644 --- a/library/init/algebra/ordered_ring.lean +++ b/library/init/algebra/ordered_ring.lean @@ -209,8 +209,7 @@ begin end instance ordered_ring.to_ordered_semiring [s : ordered_ring α] : ordered_semiring α := -{ s with - mul_zero := mul_zero, +{ mul_zero := mul_zero, zero_mul := zero_mul, add_left_cancel := @add_left_cancel α _, add_right_cancel := @add_right_cancel α _, @@ -218,7 +217,8 @@ instance ordered_ring.to_ordered_semiring [s : ordered_ring α] : ordered_semiri mul_le_mul_of_nonneg_left := @ordered_ring.mul_le_mul_of_nonneg_left α _, mul_le_mul_of_nonneg_right := @ordered_ring.mul_le_mul_of_nonneg_right α _, mul_lt_mul_of_pos_left := @ordered_ring.mul_lt_mul_of_pos_left α _, - mul_lt_mul_of_pos_right := @ordered_ring.mul_lt_mul_of_pos_right α _} + mul_lt_mul_of_pos_right := @ordered_ring.mul_lt_mul_of_pos_right α _, + ..s } section ordered_ring variable [ordered_ring α] @@ -261,8 +261,7 @@ class linear_ordered_ring (α : Type u) extends ordered_ring α, linear_order α (zero_lt_one : zero < one) instance linear_ordered_ring.to_linear_ordered_semiring [s : linear_ordered_ring α] : linear_ordered_semiring α := -{ s with - mul_zero := mul_zero, +{ mul_zero := mul_zero, zero_mul := zero_mul, add_left_cancel := @add_left_cancel α _, add_right_cancel := @add_right_cancel α _, @@ -271,7 +270,8 @@ instance linear_ordered_ring.to_linear_ordered_semiring [s : linear_ordered_ring mul_le_mul_of_nonneg_right := @mul_le_mul_of_nonneg_right α _, mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left α _, mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right α _, - le_total := linear_ordered_ring.le_total } + le_total := linear_ordered_ring.le_total, + ..s } section linear_ordered_ring variable [linear_ordered_ring α] @@ -363,8 +363,8 @@ end linear_ordered_ring class linear_ordered_comm_ring (α : Type u) extends linear_ordered_ring α, comm_monoid α instance linear_ordered_comm_ring.to_integral_domain [s: linear_ordered_comm_ring α] : integral_domain α := -{s with - eq_zero_or_eq_zero_of_mul_eq_zero := @linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero α _ } +{ eq_zero_or_eq_zero_of_mul_eq_zero := @linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero α _, + ..s } class decidable_linear_ordered_comm_ring (α : Type u) extends linear_ordered_comm_ring α, decidable_linear_ordered_comm_group α @@ -372,13 +372,13 @@ class decidable_linear_ordered_comm_ring (α : Type u) extends linear_ordered_co instance decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring [d : decidable_linear_ordered_comm_ring α] : decidable_linear_ordered_semiring α := let s : linear_ordered_semiring α := @linear_ordered_ring.to_linear_ordered_semiring α _ in -{d with - zero_mul := @linear_ordered_semiring.zero_mul α s, - mul_zero := @linear_ordered_semiring.mul_zero α s, - add_left_cancel := @linear_ordered_semiring.add_left_cancel α s, - add_right_cancel := @linear_ordered_semiring.add_right_cancel α s, - le_of_add_le_add_left := @linear_ordered_semiring.le_of_add_le_add_left α s, - mul_le_mul_of_nonneg_left := @linear_ordered_semiring.mul_le_mul_of_nonneg_left α s, - mul_le_mul_of_nonneg_right := @linear_ordered_semiring.mul_le_mul_of_nonneg_right α s, - mul_lt_mul_of_pos_left := @linear_ordered_semiring.mul_lt_mul_of_pos_left α s, - mul_lt_mul_of_pos_right := @linear_ordered_semiring.mul_lt_mul_of_pos_right α s} +{ zero_mul := @linear_ordered_semiring.zero_mul α s, + mul_zero := @linear_ordered_semiring.mul_zero α s, + add_left_cancel := @linear_ordered_semiring.add_left_cancel α s, + add_right_cancel := @linear_ordered_semiring.add_right_cancel α s, + le_of_add_le_add_left := @linear_ordered_semiring.le_of_add_le_add_left α s, + mul_le_mul_of_nonneg_left := @linear_ordered_semiring.mul_le_mul_of_nonneg_left α s, + mul_le_mul_of_nonneg_right := @linear_ordered_semiring.mul_le_mul_of_nonneg_right α s, + mul_lt_mul_of_pos_left := @linear_ordered_semiring.mul_lt_mul_of_pos_left α s, + mul_lt_mul_of_pos_right := @linear_ordered_semiring.mul_lt_mul_of_pos_right α s, + ..d } diff --git a/library/init/algebra/ring.lean b/library/init/algebra/ring.lean index 687eb709a7..3719af8ffa 100644 --- a/library/init/algebra/ring.lean +++ b/library/init/algebra/ring.lean @@ -173,9 +173,7 @@ have 0 * a + 0 = 0 * a + 0 * a, from calc show 0 * a = 0, from (add_left_cancel this).symm instance ring.to_semiring [s : ring α] : semiring α := -{ s with - mul_zero := ring.mul_zero, - zero_mul := ring.zero_mul } +{ mul_zero := ring.mul_zero, zero_mul := ring.zero_mul, ..s } lemma neg_mul_eq_neg_mul [s : ring α] (a b : α) : -(a * b) = -a * b := neg_eq_of_add_eq_zero @@ -217,9 +215,7 @@ def sub_mul := @mul_sub_right_distrib class comm_ring (α : Type u) extends ring α, comm_semigroup α instance comm_ring.to_comm_semiring [s : comm_ring α] : comm_semiring α := -{ s with - mul_zero := mul_zero, - zero_mul := zero_mul } +{ mul_zero := mul_zero, zero_mul := zero_mul, ..s } section comm_ring variable [comm_ring α] diff --git a/library/init/category/state.lean b/library/init/category/state.lean index 0d87965522..03c0dc797a 100644 --- a/library/init/category/state.lean +++ b/library/init/category/state.lean @@ -99,9 +99,9 @@ section end instance (σ : Type u) (m : Type u → Type v) [alternative m] [monad m] : alternative (state_t σ m) := -{ state_t.monad σ m with - failure := @state_t_failure σ m _ _, - orelse := @state_t_orelse σ m _ _ } +{ failure := @state_t_failure σ m _ _, + orelse := @state_t_orelse σ m _ _, + ..state_t.monad σ m } namespace state_t def read {σ : Type u} {m : Type u → Type v} [monad m] : state_t σ m σ := diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean index 693391ae9e..1fb7bbc6ed 100644 --- a/library/init/data/int/order.lean +++ b/library/init/data/int/order.lean @@ -181,8 +181,7 @@ simp [int.lt_iff_le_and_ne], split; intro h; cases h with hneq hab; split, end instance : decidable_linear_ordered_comm_ring int := -{ int.comm_ring with - le := int.le, +{ le := int.le, le_refl := int.le_refl, le_trans := @int.le_trans, le_antisymm := @int.le_antisymm, @@ -197,7 +196,8 @@ instance : decidable_linear_ordered_comm_ring int := zero_lt_one := int.zero_lt_one, decidable_eq := int.decidable_eq, decidable_le := int.decidable_le, - decidable_lt := int.decidable_lt } + decidable_lt := int.decidable_lt, + ..int.comm_ring } instance : decidable_linear_ordered_comm_group int := by apply_instance diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean index db76c8e261..981dd507bf 100644 --- a/library/init/data/list/instances.lean +++ b/library/init/data/list/instances.lean @@ -27,9 +27,9 @@ instance : monad list := end} instance : alternative list := -{ list.monad with - failure := @list.nil, - orelse := @list.append } +{ failure := @list.nil, + orelse := @list.append, + ..list.monad } instance {α : Type u} [decidable_eq α] : decidable_eq (list α) := by tactic.mk_dec_eq_instance diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index aa1df1dae1..8b77c4eea7 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -320,8 +320,7 @@ protected lemma mul_lt_mul_of_pos_right {n m k : ℕ} (h : n < m) (hk : k > 0) : mul_comm k m ▸ mul_comm k n ▸ nat.mul_lt_mul_of_pos_left h hk instance : decidable_linear_ordered_semiring nat := -{ nat.comm_semiring with - add_left_cancel := @nat.add_left_cancel, +{ add_left_cancel := @nat.add_left_cancel, add_right_cancel := @nat.add_right_cancel, lt := nat.lt, le := nat.le, @@ -339,12 +338,13 @@ instance : decidable_linear_ordered_semiring nat := mul_lt_mul_of_pos_right := @nat.mul_lt_mul_of_pos_right, decidable_lt := nat.decidable_lt, decidable_le := nat.decidable_le, - decidable_eq := nat.decidable_eq } + decidable_eq := nat.decidable_eq, + ..nat.comm_semiring } -- all the fields are already included in the decidable_linear_ordered_semiring instance instance : decidable_linear_ordered_cancel_comm_monoid ℕ := -{ nat.decidable_linear_ordered_semiring with - add_left_cancel := @nat.add_left_cancel } +{ add_left_cancel := @nat.add_left_cancel, + ..nat.decidable_linear_ordered_semiring } lemma le_of_lt_succ {m n : nat} : m < succ n → m ≤ n := le_of_succ_le_succ diff --git a/library/init/data/option/instances.lean b/library/init/data/option/instances.lean index b29bfd8123..7d59b30c57 100644 --- a/library/init/data/option/instances.lean +++ b/library/init/data/option/instances.lean @@ -31,9 +31,9 @@ def option.orelse {α : Type u} : option α → option α → option α | none none := none instance : alternative option := -{ option.monad with - failure := @none, - orelse := @option.orelse } +{ failure := @none, + orelse := @option.orelse, + ..option.monad } lemma option.eq_of_eq_some {α : Type u} : Π {x y : option α}, (∀z, x = some z ↔ y = some z) → x = y | none none h := rfl diff --git a/library/init/data/option_t.lean b/library/init/data/option_t.lean index 58829bf8ec..02bd26fa8b 100644 --- a/library/init/data/option_t.lean +++ b/library/init/data/option_t.lean @@ -60,9 +60,9 @@ show m (option α), from return none instance {m : Type u → Type v} [monad m] : alternative (option_t m) := -{ @option_t.monad m _ with - failure := @option_t_fail m _, - orelse := @option_t_orelse m _ } +{ failure := @option_t_fail m _, + orelse := @option_t_orelse m _, + ..@option_t.monad m _ } def option_t.lift {m : Type u → Type v} [monad m] {α : Type u} (a : m α) : option_t m α := (some <$> a : m (option α)) diff --git a/library/init/meta/converter/interactive.lean b/library/init/meta/converter/interactive.lean index fa9e665cd6..6052420865 100644 --- a/library/init/meta/converter/interactive.lean +++ b/library/init/meta/converter/interactive.lean @@ -135,8 +135,8 @@ rs.mmap' $ λ r, do save_info r.pos, eq_lemmas ← get_rule_eqn_lemmas r, orelse' - (do h ← to_expr' r.rule, rw_lhs h {cfg with symm := r.symm}) - (eq_lemmas.mfirst $ λ n, do e ← tactic.mk_const n, rw_lhs e {cfg with symm := r.symm}) + (do h ← to_expr' r.rule, rw_lhs h {symm := r.symm, ..cfg}) + (eq_lemmas.mfirst $ λ n, do e ← tactic.mk_const n, rw_lhs e {symm := r.symm, ..cfg}) (eq_lemmas.empty) meta def rewrite (q : parse rw_rules) (cfg : rewrite_cfg := {}) : conv unit := diff --git a/library/init/meta/interaction_monad.lean b/library/init/meta/interaction_monad.lean index ed578f380a..14c2218869 100644 --- a/library/init/meta/interaction_monad.lean +++ b/library/init/meta/interaction_monad.lean @@ -95,7 +95,7 @@ meta def interaction_monad.orelse' {α : Type u} (t₁ t₂ : m α) (use_first_e (λ e₂ ref₂ s₂', if use_first_ex then (exception e₁ ref₁ s₁') else (exception e₂ ref₂ s₂'))) meta instance interaction_monad.monad_fail : monad_fail m := -{ interaction_monad.monad with fail := λ α s, interaction_monad.fail (to_fmt s) } +{ fail := λ α s, interaction_monad.fail (to_fmt s), ..interaction_monad.monad } -- TODO: unify `parser` and `tactic` behavior? -- meta instance interaction_monad.alternative : alternative m := diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 0e5835c227..236b49c04b 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -206,9 +206,9 @@ private meta def change_core (e : expr) : option expr → tactic unit intron num_reverted /-- -`change u` replaces the target `t` of the main goal to `u` provided that `t` is well formed with respect to the local context of the main goal and `t` and `u` are definitionally equal. +`change u` replaces the target `t` of the main goal to `u` provided that `t` is well formed with respect to the local context of the main goal and `t` and `u` are definitionally equal. -`change u at h` will change a local hypothesis to `u`. +`change u at h` will change a local hypothesis to `u`. `change t with u at h1 h2 ...` will replace `t` with `u` in all the supplied hypotheses (or `*`), or in the goal if no `at` clause is specified, provided that `t` and `u` are definitionally equal. -/ @@ -239,8 +239,8 @@ meta def exacts : parse pexpr_list_or_texpr → tactic unit | [] := done | (t :: ts) := exact t >> exacts ts -/-- -A synonym for `exact` that allows writing `have/suffices/show ..., from ...` in tactic mode. +/-- +A synonym for `exact` that allows writing `have/suffices/show ..., from ...` in tactic mode. -/ meta def «from» := exact @@ -296,8 +296,8 @@ rs.mmap' $ λ r, do save_info r.pos, eq_lemmas ← get_rule_eqn_lemmas r, orelse' - (do e ← to_expr' r.rule, rewrite_target e {cfg with symm := r.symm}) - (eq_lemmas.mfirst $ λ n, do e ← mk_const n, rewrite_target e {cfg with symm := r.symm}) + (do e ← to_expr' r.rule, rewrite_target e {symm := r.symm, ..cfg}) + (eq_lemmas.mfirst $ λ n, do e ← mk_const n, rewrite_target e {symm := r.symm, ..cfg}) (eq_lemmas.empty) private meta def uses_hyp (e : expr) (h : expr) : bool := @@ -309,8 +309,8 @@ private meta def rw_hyp (cfg : rewrite_cfg) : list rw_rule → expr → tactic u save_info r.pos, eq_lemmas ← get_rule_eqn_lemmas r, orelse' - (do e ← to_expr' r.rule, when (not (uses_hyp e hyp)) $ rewrite_hyp e hyp {cfg with symm := r.symm} >>= rw_hyp rs) - (eq_lemmas.mfirst $ λ n, do e ← mk_const n, rewrite_hyp e hyp {cfg with symm := r.symm} >>= rw_hyp rs) + (do e ← to_expr' r.rule, when (not (uses_hyp e hyp)) $ rewrite_hyp e hyp {symm := r.symm, ..cfg} >>= rw_hyp rs) + (eq_lemmas.mfirst $ λ n, do e ← mk_const n, rewrite_hyp e hyp {symm := r.symm, ..cfg} >>= rw_hyp rs) (eq_lemmas.empty) meta def rw_rule_p (ep : parser pexpr) : parser rw_rule := @@ -340,7 +340,7 @@ end >> try (reflexivity reducible) `rewrite [e₁, ..., eₙ]` applies the given rules sequentially. -`rewrite e at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-` can also be used, to signify the target of the goal. +`rewrite e at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-` can also be used, to signify the target of the goal. -/ meta def rewrite (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit := rw_core q l cfg @@ -352,7 +352,7 @@ meta def rw (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) rw_core q l cfg /-- -`rewrite` followed by `assumption`. +`rewrite` followed by `assumption`. -/ meta def rwa (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit := rewrite q l cfg >> try assumption @@ -475,7 +475,7 @@ private meta def rename_lams : expr → list name → tactic unit | (lam n _ _ e) (n'::ns) := (rename n n' >> rename_lams e ns) <|> rename_lams e (n'::ns) | _ _ := skip -/-- +/-- Focuses on the `induction`/`cases` subgoal corresponding to the given introduction rule, optionally renaming introduced locals. ``` @@ -516,10 +516,10 @@ private meta def generalize_arg_p : pexpr → parser (pexpr × name) | (app (app (macro _ [const `eq _ ]) h) (local_const x _ _ _)) := pure (h, x) | _ := fail "parse error" -/-- +/-- `generalize : e = x` replaces all occurrences of `e` in the target with a new hypothesis `x` of the same type. -`generalize h : e = x` in addition registers the hypothesis `h : e = x`. +`generalize h : e = x` in addition registers the hypothesis `h : e = x`. -/ meta def generalize (h : parse ident?) (p : parse $ tk ":" *> with_desc "expr = id" (parser.pexpr 0 >>= generalize_arg_p)) : tactic unit := do let (p, x) := p, @@ -578,13 +578,13 @@ meta def cases : parse cases_arg_p → parse with_ident_list → tactic unit tactic.cases hx ids /-- -Tries to solve the current goal using a canonical proof of `true`, or the `reflexivity` tactic, or the `contradiction` tactic. +Tries to solve the current goal using a canonical proof of `true`, or the `reflexivity` tactic, or the `contradiction` tactic. -/ meta def trivial : tactic unit := tactic.triv <|> tactic.reflexivity <|> tactic.contradiction <|> fail "trivial tactic failed" -/-- -Closes the main goal using `sorry`. +/-- +Closes the main goal using `sorry`. -/ meta def admit : tactic unit := tactic.admit @@ -613,7 +613,7 @@ meta def skip : tactic unit := tactic.skip /-- -`solve1 { t }` applies the tactic `t` to the main goal and fails if it is not solved. +`solve1 { t }` applies the tactic `t` to the main goal and fails if it is not solved. -/ meta def solve1 : itactic → tactic unit := tactic.solve1 @@ -653,7 +653,7 @@ do t ← target, intro_core n >> skip /-- -Assuming the target of the goal is a Pi or a let, `assume h : t` unifies the type of the binder with `t` and introduces it with name `h`, just like `intro h`. If `h` is absent, the tactic uses the name `this`. If `t` is omitted, it will be inferred. +Assuming the target of the goal is a Pi or a let, `assume h : t` unifies the type of the binder with `t` and introduces it with name `h`, just like `intro h`. If `h` is absent, the tactic uses the name `this`. If `t` is omitted, it will be inferred. `assume (h₁ : t₁) ... (hₙ : tₙ)` introduces multiple hypotheses. Any of the types may be omitted, but the names must be present. -/ @@ -663,7 +663,7 @@ meta def «assume» : parse (sum.inl <$> (tk ":" *> texpr) <|> sum.inr <$> parse binders.mmap' $ λ b, assume_core b.local_pp_name b.local_type /-- -`have h : t := p` adds the hypothesis `h : t` to the current goal if `p` a term of type `t`. If `t` is omitted, it will be inferred. +`have h : t := p` adds the hypothesis `h : t` to the current goal if `p` a term of type `t`. If `t` is omitted, it will be inferred. `have h : t` adds the hypothesis `h : t` to the current goal and opens a new subgoal with target `t`. The new subgoal becomes the main goal. If `t` is omitted, it will be replaced by a fresh metavariable. @@ -743,8 +743,8 @@ This tactic applies to a goal such that its conclusion is an inductive type (say meta def constructor : tactic unit := tactic.constructor -/-- -Similar to `constructor`, but only non-dependent premises are added as new goals. +/-- +Similar to `constructor`, but only non-dependent premises are added as new goals. -/ meta def econstructor : tactic unit := tactic.econstructor @@ -938,7 +938,7 @@ The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or `simp [h₁ h₂ ... hₙ]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions. If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with `f` are used. This provides a convenient way to unfold `f`. `simp [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses. - + `simp *` is a shorthand for `simp [*]`. `simp only [h₁ h₂ ... hₙ]` is like `simp [h₁ h₂ ... hₙ]` but does not use `[simp]` lemmas @@ -957,7 +957,7 @@ meta def simp (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names (locat : parse location) (cfg : simp_config_ext := {}) : tactic unit := simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names locat -/-- +/-- Just construct the simp set and trace it. Used for debugging. -/ meta def trace_simp_set (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list) : tactic unit := @@ -965,7 +965,7 @@ do (s, _) ← mk_simp_set no_dflt attr_names hs, s.pp >>= trace /-- -`simp_intros h₁ h₂ ... hₙ` is similar to `intros h₁ h₂ ... hₙ` except that each hypothesis is simplified as it is introduced, and each introduced hypothesis is used to simplify later ones and the final target. +`simp_intros h₁ h₂ ... hₙ` is similar to `intros h₁ h₂ ... hₙ` except that each hypothesis is simplified as it is introduced, and each introduced hypothesis is used to simplify later ones and the final target. As with `simp`, a list of simplification lemmas can be provided. The modifiers `only` and `with` behave as with `simp`. -/ @@ -1213,14 +1213,14 @@ An abbreviation for `by_contradiction`. meta def by_contra (n : parse ident?) : tactic unit := tactic.by_contradiction n >> return () -/-- -Type check the given expression, and trace its type. +/-- +Type check the given expression, and trace its type. -/ meta def type_check (p : parse texpr) : tactic unit := do e ← to_expr p, tactic.type_check e, infer_type e >>= trace -/-- -Fail if there are unsolved goals. +/-- +Fail if there are unsolved goals. -/ meta def done : tactic unit := tactic.done @@ -1232,8 +1232,8 @@ private meta def show_aux (p : pexpr) : list expr → list expr → tactic unit <|> show_aux gs (g::r) -/-- -`show t` finds the first goal whose target unifies with `t`. It makes that the main goal, performs the unification, and replaces the target with the unified version of `t`. +/-- +`show t` finds the first goal whose target unifies with `t`. It makes that the main goal, performs the unification, and replaces the target with the unified version of `t`. -/ meta def «show» (q : parse texpr) : tactic unit := do gs ← get_goals, @@ -1285,8 +1285,8 @@ do ctx ← local_context, (mk_name_set, ff), return p.2 -/-- -Renames hypotheses with the same name. +/-- +Renames hypotheses with the same name. -/ meta def dedup : tactic unit := mwhen has_dup $ do diff --git a/library/init/meta/lean/parser.lean b/library/init/meta/lean/parser.lean index 7ea5fde13e..a1e305ddfd 100644 --- a/library/init/meta/lean/parser.lean +++ b/library/init/meta/lean/parser.lean @@ -63,9 +63,9 @@ result.cases_on (p₁ s) exception) meta instance : alternative parser := -{ interaction_monad.monad with - failure := @interaction_monad.failed _, - orelse := @parser_orelse } +{ failure := @interaction_monad.failed _, + orelse := @parser_orelse, + ..interaction_monad.monad } -- TODO: move diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 3e37ae9037..bf3749b518 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -415,7 +415,7 @@ meta structure simp_all_entry := (s : simp_lemmas) -- simplification lemmas for simplifying new_type private meta def update_simp_lemmas (es : list simp_all_entry) (h : expr) : tactic (list simp_all_entry) := -es.mmap $ λ e, do new_s ← e.s.add h, return {e with s := new_s} +es.mmap $ λ e, do new_s ← e.s.add h, return {s := new_s, ..e} /- Helper tactic for `init`. Remark: the following tactic is quadratic on the length of list expr (the list of non dependent propositions). @@ -458,7 +458,7 @@ private meta def loop (cfg : simp_config) (discharger : tactic unit) (to_unfold clear_old_hyps r | (e::es) r s m := do let ⟨h, h_type, h_pr, s'⟩ := e, - (new_h_type, new_pr) ← simplify s' to_unfold h_type {cfg with fail_if_unchanged := ff} `eq discharger, + (new_h_type, new_pr) ← simplify s' to_unfold h_type {fail_if_unchanged := ff, ..cfg} `eq discharger, if h_type =ₐ new_h_type then loop es (e::r) s m else do new_pr ← join_pr h_pr new_pr, @@ -471,7 +471,7 @@ private meta def loop (cfg : simp_config) (discharger : tactic unit) (to_unfold let new_fact_pr := mk_id_locked_proof new_h_type new_fact_pr, new_es ← update_simp_lemmas es new_fact_pr, new_r ← update_simp_lemmas r new_fact_pr, - let new_r := {e with new_type := new_h_type, pr := new_pr} :: new_r, + let new_r := {new_type := new_h_type, pr := new_pr, ..e} :: new_r, new_s ← s.add new_fact_pr, loop new_es new_r new_s tt diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean index fa0b5ebf3d..1f6473bb51 100644 --- a/library/init/meta/smt/smt_tactic.lean +++ b/library/init/meta/smt/smt_tactic.lean @@ -43,7 +43,7 @@ structure smt_config := (em_attr : name := `ematch) meta def smt_config.set_classical (c : smt_config) (b : bool) : smt_config := -{c with cc_cfg := { (c.cc_cfg) with em := b}} +{ cc_cfg := { em := b, ..c.cc_cfg }, ..c } meta constant smt_goal : Type meta def smt_state := @@ -80,12 +80,12 @@ meta def smt_tactic_orelse {α : Type} (t₁ t₂ : smt_tactic α) : smt_tactic result.exception) meta instance : monad_fail smt_tactic := -{ smt_tactic.monad with fail := λ α s, (tactic.fail (to_fmt s) : smt_tactic α) } +{ fail := λ α s, (tactic.fail (to_fmt s) : smt_tactic α), ..smt_tactic.monad } meta instance : alternative smt_tactic := -{ smt_tactic.monad with - failure := λ α, @tactic.failed α, - orelse := @smt_tactic_orelse } +{ failure := λ α, @tactic.failed α, + orelse := @smt_tactic_orelse, + ..smt_tactic.monad } namespace smt_tactic open tactic (transparency) diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index dc4753bb67..7705eadfc9 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -59,9 +59,9 @@ infixl ` >>=[tactic] `:2 := interaction_monad_bind infixl ` >>[tactic] `:2 := interaction_monad_seq meta instance : alternative tactic := -{ interaction_monad.monad with - failure := @interaction_monad.failed _, - orelse := @interaction_monad_orelse _ } +{ failure := @interaction_monad.failed _, + orelse := @interaction_monad_orelse _, + ..interaction_monad.monad } meta def {u₁ u₂} tactic.up {α : Type u₂} (t : tactic α) : tactic (ulift.{u₁} α) := λ s, match t s with diff --git a/library/system/io.lean b/library/system/io.lean index a549789d95..75138b2fac 100644 --- a/library/system/io.lean +++ b/library/system/io.lean @@ -90,8 +90,7 @@ protected def io.fail {α : Type} (s : string) : io α := io.interface.fail io.error α (io.error.other s) instance : monad_fail io := -{ io_core_is_monad io.error with - fail := @io.fail _ } +{ fail := @io.fail _, ..io_core_is_monad io.error } namespace io def iterate {e α} (a : α) (f : α → io_core e (option α)) : io_core e α := @@ -112,9 +111,9 @@ match res with end instance : alternative io := -{ interface.monad _ with - orelse := λ _ a b, catch a (λ _, b), - failure := λ _, io.fail "failure" } +{ orelse := λ _ a b, catch a (λ _, b), + failure := λ _, io.fail "failure", + ..interface.monad _ } def put_str : string → io unit := interface.term.put_str @@ -232,7 +231,7 @@ format.print (to_fmt a) read into `string` which is then returned. -/ def io.cmd (args : io.process.spawn_args) : io string := -do child ← io.proc.spawn { args with stdout := io.process.stdio.piped }, +do child ← io.proc.spawn { stdout := io.process.stdio.piped, ..args }, buf ← io.fs.read_to_end child.stdout, exitv ← io.proc.wait child, when (exitv ≠ 0) $ io.fail $ "process exited with status " ++ repr exitv, diff --git a/library/tools/debugger/cli.lean b/library/tools/debugger/cli.lean index ece6579a75..b5470ba10d 100644 --- a/library/tools/debugger/cli.lean +++ b/library/tools/debugger/cli.lean @@ -47,7 +47,7 @@ match args with fn ← return $ to_qualified_name arg, ok ← is_valid_fn_prefix fn, if ok then - return {s with fn_bps := fn :: list.filter (λ fn', fn ≠ fn') s.fn_bps} + return { fn_bps := fn :: list.filter (λ fn', fn ≠ fn') s.fn_bps, ..s } else vm.put_str "invalid 'break' command, given name is not the prefix for any function\n" >> return s @@ -60,7 +60,7 @@ meta def remove_breakpoint (s : state) (args : list string) : vm state := match args with | [arg] := do fn ← return $ to_qualified_name arg, - return {s with fn_bps := list.filter (λ fn', fn ≠ fn') s.fn_bps} + return { fn_bps := list.filter (λ fn', fn ≠ fn') s.fn_bps, ..s } | _ := vm.put_str "invalid 'rbreak ' command, incorrect number of arguments\n" >> return s @@ -128,7 +128,7 @@ meta def cmd_loop_core : state → nat → list string → vm state is_eof ← vm.eof, if is_eof then do vm.put_str "stopping debugger... 'end of file' has been found\n", - return {s with md := mode.done } + return { md := mode.done, ..s } else do vm.put_str "% ", l ← vm.get_line, @@ -138,9 +138,9 @@ meta def cmd_loop_core : state → nat → list string → vm state | [] := cmd_loop_core s frame default_cmd | (cmd::args) := if cmd = "help" ∨ cmd = "h" then show_help >> cmd_loop_core s frame [] - else if cmd = "exit" then return {s with md := mode.done } - else if cmd = "run" ∨ cmd = "r" then return {s with md := mode.run } - else if cmd = "step" ∨ cmd = "s" then return {s with md := mode.step } + else if cmd = "exit" then return { md := mode.done, ..s } + else if cmd = "run" ∨ cmd = "r" then return { md := mode.run, ..s } + else if cmd = "step" ∨ cmd = "s" then return { md := mode.step, ..s } else if cmd = "break" ∨ cmd = "b" then do new_s ← add_breakpoint s args, cmd_loop_core new_s frame [] else if cmd = "rbreak" then do new_s ← remove_breakpoint s args, cmd_loop_core new_s frame [] else if cmd = "bs" then do @@ -166,20 +166,20 @@ def prune_active_bps_core (csz : nat) : list (nat × name) → list (nat × name meta def prune_active_bps (s : state) : vm state := do sz ← vm.call_stack_size, - return {s with active_bps := prune_active_bps_core sz s.active_bps} + return { active_bps := prune_active_bps_core sz s.active_bps, ..s } meta def updt_csz (s : state) : vm state := do sz ← vm.call_stack_size, - return {s with csz := sz} + return { csz := sz, ..s } meta def init_transition (s : state) : vm state := do opts ← vm.get_options, - if opts.get_bool `server ff then return {s with md := mode.done} + if opts.get_bool `server ff then return { md := mode.done, ..s } else do bps ← vm.get_attribute `breakpoint, - new_s ← return {s with fn_bps := bps}, + new_s ← return { fn_bps := bps, ..s }, if opts.get_bool `debugger.autorun ff then - return {new_s with md := mode.run} + return { md := mode.run, ..new_s } else do vm.put_str "Lean debugger\n", show_curr_fn "debugging", @@ -215,7 +215,7 @@ do b1 ← in_active_bps s, show_curr_fn "breakpoint", fn ← vm.curr_fn, sz ← vm.call_stack_size, - new_s ← return $ {s with active_bps := (sz, fn) :: s.active_bps}, + new_s ← return $ { active_bps := (sz, fn) :: s.active_bps, ..s }, cmd_loop new_s ["r"] meta def step_fn (s : state) : vm state :=