max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(*): remove end after each match-expression

Browse source 
`end` is not optional anymore
This commit is contained in:
Leonardo de Moura 2018-05-04 11:27:21 -07:00
parent 752e0a134e
commit d5fe509c36
33 changed files with 131 additions and 263 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/control/except.lean
View file

@ -50,7 +50,6 @@ section
match ma with
| (except.error err) := except.error err
| (except.ok v) := f v
end
protected def to_bool {α : Type v} : except ε α → bool
| (except.ok _) := tt
@ -94,8 +93,7 @@ section
protected def catch {α : Type u} (ma : except_t ε m α) (handle : ε → except_t ε m α) : except_t ε m α :=
⟨ma.run >>= λ res, match res with
| except.ok a := pure (except.ok a)
| except.error e := (handle e).run
end⟩
| except.error e := (handle e).run⟩
@[inline] protected def monad_map {m'} [monad m'] {α} (f : ∀ {α}, m α → m' α) : except_t ε m α → except_t ε m' α :=
λ x, ⟨f x.run⟩

1
library/init/data/bool/lemmas.lean
View file

@ -111,7 +111,6 @@ show (tt = tt) = true, by simp
match d with
| is_true hp := ⟨λh, hp, λ_, rfl⟩
| is_false hnp := ⟨λh, bool.no_confusion h, λhp, absurd hp hnp⟩
end
theorem to_bool_true {p : Prop} [decidable p] : p → to_bool p := (to_bool_iff p).2

5
library/init/data/hashmap/basic.lean
View file

@ -114,17 +114,14 @@ variables {α : Type u} {β : α → Type v} [decidable_eq α] {h : α → usize
def insert (m : d_hashmap α β h) (a : α) (b : β a) : d_hashmap α β h :=
match m with
| ⟨ m, hw ⟩ := ⟨ m.insert h a b, well_formed.insert_wff m a b hw ⟩
end
def erase (m : d_hashmap α β h) (a : α) : d_hashmap α β h :=
match m with
| ⟨ m, hw ⟩ := ⟨ m.erase h a, well_formed.erase_wff m a hw ⟩
end
def find (m : d_hashmap α β h) (a : α) : option (β a) :=
match m with
| ⟨ m, _ ⟩ := m.find h a
end
@[inline] def contains (m : d_hashmap α β h) (a : α) : bool :=
(m.find a).is_some
@ -132,12 +129,10 @@ end
def fold {δ : Type w} (m : d_hashmap α β h) (d : δ) (f : δ → Π a, β a → δ) : δ :=
match m with
| ⟨ m, _ ⟩ := m.fold d f
end
def size (m : d_hashmap α β h) : nat :=
match m with
| ⟨ {size := sz, ..}, _ ⟩ := sz
end
@[inline] def empty (m : d_hashmap α β h) : bool :=
m.size = 0

1
library/init/data/int/basic.lean
View file

@ -57,7 +57,6 @@ def sub_nat_nat (m n : ℕ) : int :=
match (n - m : nat) with
| 0 := of_nat (m - n) -- m ≥ n
| (succ k) := -[1+ k] -- m < n, and n - m = succ k
end
protected def neg : int → int
| (of_nat n) := neg_of_nat n

18
library/init/data/list/basic.lean
View file

@ -23,12 +23,10 @@ protected def has_dec_eq [s : decidable_eq α] : decidable_eq (list α)
| (a::as) (b::bs) :=
match s a b with
| is_true hab :=
match has_dec_eq as bs with
| is_true habs := is_true (eq.subst hab (eq.subst habs rfl))
| is_false nabs := is_false (λ h, list.no_confusion h (λ _ habs, absurd habs nabs))
end
(match has_dec_eq as bs with
| is_true habs := is_true (eq.subst hab (eq.subst habs rfl))
| is_false nabs := is_false (λ h, list.no_confusion h (λ _ habs, absurd habs nabs)))
| is_false nab := is_false (λ h, list.no_confusion h (λ hab _, absurd hab nab))
end
instance [decidable_eq α] : decidable_eq (list α) :=
list.has_dec_eq
@ -61,9 +59,8 @@ instance decidable_mem [decidable_eq α] (a : α) : ∀ (l : list α), decidable
| (b::l) :=
if h₁ : a = b then is_true (or.inl h₁)
else match decidable_mem l with
| is_true h₂ := is_true (or.inr h₂)
| is_false h₂ := is_false (not_or h₁ h₂)
end
| is_true h₂ := is_true (or.inr h₂)
| is_false h₂ := is_false (not_or h₁ h₂)
instance : has_emptyc (list α) :=
⟨list.nil⟩
@ -135,7 +132,6 @@ def filter_map (f : α → option β) : list α → list β
match f a with
| none := filter_map l
| some b := b :: filter_map l
end
def filter (p : α → Prop) [decidable_pred p] : list α → list α
| [] := []
@ -209,7 +205,7 @@ zip_with prod.mk
def unzip : list (α × β) → list α × list β
| [] := ([], [])
| ((a, b) :: t) := match unzip t with (al, bl) := (a::al, b::bl) end
| ((a, b) :: t) := match unzip t with | (al, bl) := (a::al, b::bl)
protected def insert [decidable_eq α] (a : α) (l : list α) : list α :=
if a ∈ l then l else a :: l
@ -300,8 +296,6 @@ instance has_decidable_lt [has_lt α] [h : decidable_rel ((<) : α → α → Pr
match has_decidable_lt as bs with
| is_true h₂ := is_true (or.inr h₂)
| is_false h₂ := is_false (λ hd, or.elim hd (λ n₁, absurd n₁ h₁) (λ n₂, absurd n₂ h₂))
end
end
@[reducible] protected def le [has_lt α] (a b : list α) : Prop :=
¬ b < a

3
library/init/data/option/basic.lean
View file

@ -43,7 +43,7 @@ protected def map {α β} (f : α → β) (o : option α) : option β :=
option.bind o (some ∘ f)
theorem map_id {α} : (option.map id : option α → option α) = id :=
funext (λo, match o with | none := rfl | some x := rfl end)
funext (λo, match o with | none := rfl | some x := rfl)
instance : monad option :=
{pure := @some, bind := @option.bind, map := @option.map}
@ -81,6 +81,5 @@ instance {α : Type u} [d : decidable_eq α] : decidable_eq (option α)
match (d v₁ v₂) with
| (is_true e) := is_true (congr_arg (@some α) e)
| (is_false n) := is_false (λ h, option.no_confusion h (λ e, absurd e n))
end
instance {α : Type u} [has_lt α] : has_lt (option α) := ⟨option.lt (<)⟩

22
library/init/data/ordering/basic.lean
View file

@ -12,7 +12,7 @@ inductive ordering
| lt | eq | gt
instance : has_repr ordering :=
⟨(λ s, match s with | ordering.lt := "lt" | ordering.eq := "eq" | ordering.gt := "gt" end)⟩
⟨(λ s, match s with | ordering.lt := "lt" | ordering.eq := "eq" | ordering.gt := "gt")⟩
namespace ordering
def swap : ordering → ordering
@ -43,21 +43,17 @@ instance : decidable_eq ordering :=
λ a b,
match a with
| ordering.lt :=
match b with
| ordering.lt := is_true rfl
| ordering.eq := is_false (λ h, ordering.no_confusion h)
| ordering.gt := is_false (λ h, ordering.no_confusion h)
end
(match b with
| ordering.lt := is_true rfl
| ordering.eq := is_false (λ h, ordering.no_confusion h)
| ordering.gt := is_false (λ h, ordering.no_confusion h))
| ordering.eq :=
match b with
| ordering.lt := is_false (λ h, ordering.no_confusion h)
| ordering.eq := is_true rfl
| ordering.gt := is_false (λ h, ordering.no_confusion h)
end
(match b with
| ordering.lt := is_false (λ h, ordering.no_confusion h)
| ordering.eq := is_true rfl
| ordering.gt := is_false (λ h, ordering.no_confusion h))
| ordering.gt :=
match b with
| ordering.lt := is_false (λ h, ordering.no_confusion h)
| ordering.eq := is_false (λ h, ordering.no_confusion h)
| ordering.gt := is_true rfl
end
end

2
library/init/data/rbmap/basic.lean
View file

@ -50,7 +50,6 @@ match m.val with
| rbnode.leaf := false
| rbnode.red_node _ e _ := rbtree.mem (k, e.2) m
| rbnode.black_node _ e _ := rbtree.mem (k, e.2) m
end
instance : has_mem α (rbmap α β lt) :=
⟨rbmap.mem⟩
@ -71,7 +70,6 @@ match m.val with
| rbnode.leaf := none
| rbnode.red_node _ e _ := @rbtree.find _ _ rbmap_lt_dec m (k, e.2)
| rbnode.black_node _ e _ := @rbtree.find _ _ rbmap_lt_dec m (k, e.2)
end
def to_value : option (α × β) → option β
| none := none

28
library/init/data/rbtree/basic.lean
View file

@ -96,11 +96,10 @@ variables (lt : α → α → Prop) [decidable_rel lt]
def ins : rbnode α → α → rbnode α
| leaf x := red_node leaf x leaf
| (red_node a y b) x :=
match cmp_using lt x y with
| ordering.lt := red_node (ins a x) y b
| ordering.eq := red_node a x b
| ordering.gt := red_node a y (ins b x)
end
(match cmp_using lt x y with
| ordering.lt := red_node (ins a x) y b
| ordering.eq := red_node a x b
| ordering.gt := red_node a y (ins b x))
| (black_node a y b) x :=
match cmp_using lt x y with
| ordering.lt :=
@ -110,7 +109,6 @@ def ins : rbnode α → α → rbnode α
| ordering.gt :=
if b.get_color = red then balance2_node (ins b x) y a
else black_node a y (ins b x)
end
def mk_insert_result : color → rbnode α → rbnode α
| red (red_node l v r) := black_node l v r
@ -140,17 +138,15 @@ variable [decidable_rel lt]
def find : rbnode α → α → option α
| leaf x := none
| (red_node a y b) x :=
match cmp_using lt x y with
| ordering.lt := find a x
| ordering.eq := some y
| ordering.gt := find b x
end
(match cmp_using lt x y with
| ordering.lt := find a x
| ordering.eq := some y
| ordering.gt := find b x)
| (black_node a y b) x :=
match cmp_using lt x y with
| ordering.lt := find a x
| ordering.eq := some y
| ordering.gt := find b x
end
(match cmp_using lt x y with
| ordering.lt := find a x
| ordering.eq := some y
| ordering.gt := find b x)
end membership

4
library/init/data/repr.lean
View file

@ -38,10 +38,10 @@ instance : has_repr unit :=
⟨λ u, "()"⟩
instance {α : Type u} [has_repr α] : has_repr (option α) :=
⟨λ o, match o with | none := "none" | (some a) := "(some " ++ repr a ++ ")" end⟩
⟨λ o, match o with | none := "none" | (some a) := "(some " ++ repr a ++ ")"⟩
instance {α : Type u} {β : Type v} [has_repr α] [has_repr β] : has_repr (α ⊕ β) :=
⟨λ s, match s with | (inl a) := "(inl " ++ repr a ++ ")" | (inr b) := "(inr " ++ repr b ++ ")" end⟩
⟨λ s, match s with | (inl a) := "(inl " ++ repr a ++ ")" | (inr b) := "(inr " ++ repr b ++ ")"⟩
instance {α : Type u} {β : Type v} [has_repr α] [has_repr β] : has_repr (α × β) :=
⟨λ ⟨a, b⟩, "(" ++ repr a ++ ", " ++ repr b ++ ")"⟩

9
library/init/data/string/basic.lean
View file

@ -126,16 +126,14 @@ protected def extract_core : list char → list char → option (list char)
match extract_core cs₁ cs₂ with
| none := none
| some r := some (c::r)
end
def extract : iterator → iterator → option string
| ⟨p₁, n₁⟩ ⟨p₂, n₂⟩ :=
if p₁.reverse ++ n₁ ≠ p₂.reverse ++ n₂ then none
else if n₁ = n₂ then some ""
else match iterator.extract_core n₁ n₂ with
| none := none
| some r := some ⟨r⟩
end
else (match iterator.extract_core n₁ n₂ with
| none := none
| some r := some ⟨r⟩)
end iterator
end string
@ -201,7 +199,6 @@ private def line_column_aux : nat → string.iterator → nat × nat → nat ×
else match it.curr with
| '\n' := line_column_aux k it.next (line+1, 0)
| other := line_column_aux k it.next (line, col+1)
end
def line_column (s : string) (offset : nat) : nat × nat :=
line_column_aux offset s.mk_iterator (1, 0)

4
library/init/data/to_string.lean
View file

@ -62,10 +62,10 @@ instance : has_to_string uint64 :=
⟨λ n, to_string (fin.val n)⟩
instance {α : Type u} [has_to_string α] : has_to_string (option α) :=
⟨λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")" end⟩
⟨λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")"⟩
instance {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] : has_to_string (α ⊕ β) :=
⟨λ s, match s with | (inl a) := "(inl " ++ to_string a ++ ")" | (inr b) := "(inr " ++ to_string b ++ ")" end⟩
⟨λ s, match s with | (inl a) := "(inl " ++ to_string a ++ ")" | (inr b) := "(inr " ++ to_string b ++ ")"⟩
instance {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] : has_to_string (α × β) :=
⟨λ ⟨a, b⟩, "(" ++ to_string a ++ ", " ++ to_string b ++ ")"⟩

1
library/init/lean/disjoint_set.lean
View file

@ -33,7 +33,6 @@ private def find_aux : nat → α → hashmap α (node α) h → node α
match m.find a with
| some r := if r.find = a then r else find_aux n r.find m
| none := { find := a, rank := 0 }
end
def find : disjoint_set α h → α → α
| ⟨m⟩ a := (find_aux m.size a m).find

8
library/init/lean/ir/check.lean
View file

@ -141,8 +141,7 @@ p.ys.mfoldl (λ s y,
then do b ← read_block,
throw (ssa_error.phi_multiple_entries b.id p.x bid)
else return $ (s.insert bid)
| none := do b ← read_block, throw (ssa_error.undefined b.id y)
end)
| none := do b ← read_block, throw (ssa_error.undefined b.id y))
mk_blockid_set
def phis.check_predecessors (ps : list phi) : ssa_valid_m unit :=
@ -152,8 +151,8 @@ do ps.mfoldl (λ (os : option blockid_set) (p : phi),
| (some s) := if s.seteq s' then return os
else do b ← read_block,
throw (ssa_error.phi_missing_predecessor b.id p.x)
| none := return (some s')
end) none,
| none := return (some s'))
none,
return ()
def block.valid_ssa_core : ssa_valid_m unit :=
@ -179,7 +178,6 @@ do m ← d.var2blockid,
bs.mmap' (λ b : block, run_reader block.valid_ssa (m, b)),
return m
| _ := return m
end
/- Check blockids -/
inductive blockid_error

2
library/init/lean/name.lean
View file

@ -52,14 +52,12 @@ instance has_decidable_eq : decidable_eq name
match has_decidable_eq p₁ p₂ with
| is_true h₂ := is_true $ h₁ ▸ h₂ ▸ rfl
| is_false h₂ := is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hp h₂
end
else is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hs h₁
| (mk_numeral p₁ n₁) (mk_numeral p₂ n₂) :=
if h₁ : n₁ = n₂ then
match has_decidable_eq p₁ p₂ with
| is_true h₂ := is_true $ h₁ ▸ h₂ ▸ rfl
| is_false h₂ := is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hp h₂
end
else is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hs h₁
| anonymous (mk_string _ _) := is_false $ λ h, name.no_confusion h
| anonymous (mk_numeral _ _) := is_false $ λ h, name.no_confusion h

43
library/init/lean/parser/parser.lean
View file

@ -64,7 +64,6 @@ match p s.mk_iterator with
| ok a _ := except.ok a
| ok_eps a _ _ := except.ok a
| error msg _ := except.error msg
end
@[inline] def mk_eps_result (a : α) (it : iterator) : result α :=
ok_eps a it dlist.empty
@ -91,19 +90,16 @@ def merge (msg₁ msg₂ : message) : message :=
protected def bind (p : parser α) (q : α → parser β) : parser β :=
λ it, match p it with
| ok a it :=
match q a it with
| ok_eps b it msg₂ := ok b it
| error msg ff := error msg tt
| other := other
end
(match q a it with
| ok_eps b it msg₂ := ok b it
| error msg ff := error msg tt
| other := other)
| ok_eps a it ex₁ :=
match q a it with
| ok_eps b it ex₂ := ok_eps b it (ex₁ ++ ex₂)
| error msg₂ ff := error { expected := ex₁ ++ msg₂.expected, .. msg₂ } ff
| other := other
end
(match q a it with
| ok_eps b it ex₂ := ok_eps b it (ex₁ ++ ex₂)
| error msg₂ ff := error { expected := ex₁ ++ msg₂.expected, .. msg₂ } ff
| other := other)
| error msg c := error msg c
end
instance : monad parser :=
{ bind := @parser.bind, pure := @parser.pure }
@ -116,7 +112,6 @@ def expect (msg : message) (exp : string) : message :=
| ok_eps a it _ := ok_eps a it (dlist.singleton ex)
| error msg ff := error (expect msg ex) ff
| other := other
end
infixr ` <?> `:2 := label
@ -141,7 +136,6 @@ def try (p : parser α) : parser α :=
λ it, match p it with
| error msg _ := error msg ff
| other := other
end
/--
The `orelse p q` combinator behaves as follows:
@ -161,19 +155,16 @@ def try (p : parser α) : parser α :=
protected def orelse (p q : parser α) : parser α :=
λ it, match p it with
| ok_eps a it' ex₁ :=
match q it with
| ok_eps _ _ ex₂ := ok_eps a it' (ex₁ ++ ex₂)
| error msg₂ ff := ok_eps a it' (ex₁ ++ msg₂.expected)
| other := other
end
(match q it with
| ok_eps _ _ ex₂ := ok_eps a it' (ex₁ ++ ex₂)
| error msg₂ ff := ok_eps a it' (ex₁ ++ msg₂.expected)
| other := other)
| error msg₁ ff :=
match q it with
| ok_eps a it' ex₂ := ok_eps a it' (msg₁.expected ++ ex₂)
| error msg₂ ff := error (merge msg₁ msg₂) ff
| other := other
end
(match q it with
| ok_eps a it' ex₂ := ok_eps a it' (msg₁.expected ++ ex₂)
| error msg₂ ff := error (merge msg₁ msg₂) ff
| other := other)
| other := other
end
instance : alternative parser :=
{ orelse := @parser.orelse,
@ -400,7 +391,6 @@ def lookahead (p : parser α) : parser α :=
λ it, match p it with
| ok a s' := mk_eps_result a it
| other := other
end
/-- `not_followed_by p` succeeds when parser `p` fails -/
def not_followed_by (p : parser α) (msg : string := "input") : parser unit :=
@ -408,7 +398,6 @@ def not_followed_by (p : parser α) (msg : string := "input") : parser unit :=
| ok _ _ := error { pos := it.offset, unexpected := msg } ff
| ok_eps _ _ _ := error { pos := it.offset, unexpected := msg } ff
| error _ _ := mk_eps_result () it
end
/-- Faster version of `not_followed_by (satisfy p)` -/
@[inline] def not_followed_by_sat (p : char → bool) : parser unit :=

1
library/init/meta/contradiction_tactic.lean
View file

@ -68,7 +68,6 @@ private meta def contra_constructor_eq : list expr → tactic unit
exact pr
else contra_constructor_eq Hs
| _ := contra_constructor_eq Hs
end
meta def contradiction : tactic unit :=
do try intro1,

10
library/init/meta/decl_cmds.lean
View file

@ -11,12 +11,10 @@ private meta def apply_replacement (replacements : name_map name) (e : expr) : e
e.replace (λ e d,
match e with
| expr.const n ls :=
match replacements.find n with
| some new_n := some (expr.const new_n ls)
| none := none
end
| _ := none
end)
(match replacements.find n with
| some new_n := some (expr.const new_n ls)
| none := none)
| _ := none)
/-- Given a set of constant renamings `replacements` and a declaration name `src_decl_name`, create a new
declaration called `new_decl_name` s.t. its type is the type of `src_decl_name` after applying the

4
library/init/meta/environment.lean
View file

@ -35,7 +35,7 @@ meta def contains (env : environment) (d : name) : bool :=
match env.get d with
| exceptional.success _ := tt
| exceptional.exception ._ _ := ff
end
/-- Register the given name as a namespace, making it available to the `open` command -/
meta constant add_namespace : environment → name → environment
/-- Return tt iff the given name is a namespace -/
@ -105,7 +105,6 @@ match (refl_for env (const_name (get_app_fn e))) with
then some (n, app_arg (app_fn e), app_arg e)
else none
| none := none
end
/-- Return true if 'n' has been declared in the current file -/
meta def in_current_file (env : environment) (n : name) : bool :=
@ -115,7 +114,6 @@ meta def is_definition (env : environment) (n : name) : bool :=
match env.get n with
| exceptional.success (declaration.defn _ _ _ _ _ _) := tt
| _ := ff
end
end environment

5
library/init/meta/expr.lean
View file

@ -29,8 +29,7 @@ instance : has_repr binder_info :=
| binder_info.implicit := "implicit"
| binder_info.strict_implicit := "strict_implicit"
| binder_info.inst_implicit := "inst_implicit"
| binder_info.aux_decl := "aux_decl"
end⟩
| binder_info.aux_decl := "aux_decl"⟩
meta constant macro_def : Type
@ -64,7 +63,6 @@ meta def expr.erase_annotations : expr elab → expr elab
match e.is_annotation with
| some (_, a) := expr.erase_annotations a
| none := e
end
/-- Compares expressions, including binder names. -/
meta constant expr.has_decidable_eq : decidable_eq expr
@ -147,7 +145,6 @@ id
λ ef ea, match ef with
| (expr.lam _ _ _ _) := expr.subst ef ea
| _ := expr.app ef ea
end
attribute [irreducible] reflected reflected.subst reflected.to_expr

1
library/init/meta/injection_tactic.lean
View file

@ -73,7 +73,6 @@ private meta def injections_with_inner : nat → list expr → list name → tac
| none := injections_with_inner (n+1) lc ns
| some ([], _) := skip -- This means that the contradiction part was triggered and the goal is done
| some (t, ns') := injections_with_inner n (t ++ lc) ns'
end
meta def injections_with (ns : list name) : tactic unit :=
do lc ← local_context,

139
library/init/meta/interactive.lean
View file

@ -73,12 +73,10 @@ let aux (n : name) : tactic expr := do
match p with
| (expr.const c []) := do r ← mk_const c, save_type_info r q, return r
| _ := i_to_expr p
end
in match q with
| (expr.const c []) := aux c
| (expr.local_const c _ _ _) := aux c
| _ := i_to_expr q
end
namespace interactive
open interactive interactive.types expr
@ -108,8 +106,7 @@ mcond tags_enabled
r ← r.mfilter $ λ ⟨n, m⟩, bnot <$> is_assigned m,
match r with
| [(_, m)] := set_tag m in_tag /- if there is only new subgoal, we just propagate `in_tag` -/
| _ := r.mmap' (λ ⟨n, m⟩, set_tag m (n::in_tag))
end)
| _ := r.mmap' (λ ⟨n, m⟩, set_tag m (n::in_tag)))
(tac >> skip)
/--
@ -289,9 +286,7 @@ do {
p ← resolve_name n,
match p with
| expr.const n _ := mk_const n -- create metavars for universe levels
| _ := i_to_expr p
end
}
| _ := i_to_expr p }
/- Version of to_expr that tries to bypass the elaborator if `p` is just a constant or local constant.
This is not an optimization, by skipping the elaborator we make sure that no unwanted resolution is used.
@ -302,7 +297,6 @@ match p with
| (const c []) := do new_e ← resolve_name' c, save_type_info new_e p, return new_e
| (local_const c _ _ _) := do new_e ← resolve_name' c, save_type_info new_e p, return new_e
| _ := i_to_expr p
end
meta structure rw_rule :=
(pos : pos)
@ -319,13 +313,11 @@ let aux (n : name) : tactic (list name) := do {
let e := p.erase_annotations.get_app_fn.erase_annotations,
match e with
| const n _ := get_eqn_lemmas_for tt n
| _ := return []
end } <|> return [] in
| _ := return [] } <|> return [] in
match r.rule with
| const n _ := aux n
| local_const n _ _ _ := aux n
| _ := return []
end
private meta def rw_goal (cfg : rewrite_cfg) (rs : list rw_rule) : tactic unit :=
rs.mmap' $ λ r, do
@ -367,11 +359,11 @@ meta def rw_rules : parser rw_rules_t :=
<|> rw_rules_t.mk <$> (list.ret <$> rw_rule_p texpr) <*> return none
private meta def rw_core (rs : parse rw_rules) (loca : parse location) (cfg : rewrite_cfg) : tactic unit :=
match loca with
| loc.wildcard := loca.try_apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules)
| _ := loca.apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules)
end >> try (reflexivity reducible)
>> (returnopt rs.end_pos >>= save_info <|> skip)
(match loca with
| loc.wildcard := loca.try_apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules)
| _ := loca.apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules))
>> try (reflexivity reducible)
>> (returnopt rs.end_pos >>= save_info <|> skip)
/--
`rewrite e` applies identity `e` as a rewrite rule to the target of the main goal. If `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction. If `e` is a defined constant, then the equational lemmas associated with `e` are used. This provides a convenient way to unfold `e`.
@ -486,7 +478,6 @@ with_desc "(id :)? expr" $ do
| (local_const x _ _ _) :=
(tk ":" *> do t ← texpr, pure (some x, t)) <|> pure (none, t)
| _ := pure (none, t)
end
/--
Given the initial tag `in_tag` and the cases names produced by `induction` or `cases` tactic,
@ -509,7 +500,6 @@ do te ← tags_enabled,
```
-/
else tgs.mmap' (λ ⟨n, g⟩, with_enable_tags (set_tag g (`_case_simple::n::[])))
end
private meta def set_induction_tags (in_tag : tag) (rs : list (name × list expr × list (name × expr))) : tactic unit :=
set_cases_tags in_tag (rs.map (λ e, e.1))
@ -534,14 +524,12 @@ meta def induction (hp : parse cases_arg_p) (rec_name : parse using_ident) (ids
do in_tag ← get_main_tag,
focus1 $ do {
-- process `h : t` case
e ← match hp with
| (some h, p) := do
x ← get_unused_name,
generalize h () (p, x),
get_local x
| (none, p) := i_to_expr p
end,
e ← (match hp with
| (some h, p) := do
x ← get_unused_name,
generalize h () (p, x),
get_local x
| (none, p) := i_to_expr p),
-- generalize major premise
e ← if e.is_local_constant then pure e
else tactic.generalize e >> intro1,
@ -612,7 +600,6 @@ do gs ← collect_tagged_goals pre,
| gs := do
tags : list (list name) ← gs.mmap get_tag,
fail ("invalid `case`, there is more than one goal tagged with prefix " ++ to_string pre ++ ", matching tags: " ++ to_string tags)
end
private meta def find_tagged_goal (pre : list name) : tactic expr :=
match pre with
@ -628,7 +615,6 @@ match pre with
else return r_id)
<|> return id),
find_tagged_goal_aux pre
end
private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indices : nat) : option expr → expr → option (expr × expr)
| case e := if e.has_meta_var then match e with
@ -638,34 +624,30 @@ private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indi
pure (case, e)
| (app _ _) :=
let idx :=
match e.get_app_fn with
(match e.get_app_fn with
| const (name.mk_string rec ty') _ :=
guard (ty' = ty) >>
match mk_simple_name rec with
| `drec := some idx | `rec := some idx
-- indices + major premise
| `dcases_on := some (idx + num_indices + 1) | `cases_on := some (idx + num_indices + 1)
| _ := none
end
| _ := none
end in
match idx with
| none := list.foldl (<|>) (find_case case e.get_app_fn) $ e.get_app_args.map (find_case case)
| some idx :=
let args := e.get_app_args in
do arg ← args.nth idx,
(match mk_simple_name rec with
| `drec := some idx | `rec := some idx
-- indices + major premise
| `dcases_on := some (idx + num_indices + 1) | `cases_on := some (idx + num_indices + 1)
| _ := none)
| _ := none) in
(match idx with
| none := list.foldl (<|>) (find_case case e.get_app_fn) $ e.get_app_args.map (find_case case)
| some idx :=
let args := e.get_app_args in
do arg ← args.nth idx,
args.enum.foldl
(λ acc ⟨i, arg⟩, match acc with
| some _ := acc
| _ := if i ≠ idx then find_case none arg else none
end)
| _ := if i ≠ idx then find_case none arg else none)
-- start recursion with likely case
(find_case (some arg) arg)
end
(find_case (some arg) arg))
| (lam _ _ _ e) := find_case case e
| (macro n args) := list.foldl (<|>) none $ args.map (find_case case)
| _ := none
end else none
else none
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)
@ -718,8 +700,6 @@ do g ← find_tagged_goal pre,
rename_lams case ids,
solve1 tac
| ff := failed
end
end
/--
Assuming `x` is a variable in the local context with an inductive type, `destruct x` splits the main goal, producing one goal for each constructor of the inductive type, in which `x` is assumed to be a general instance of that constructor. In contrast to `cases`, the local context is unchanged, i.e. no elements are reverted or introduced.
@ -838,7 +818,6 @@ meta def iterate (n : parse small_nat?) (t : itactic) : tactic unit :=
match n with
| none := tactic.iterate t
| some n := iterate_exactly n t
end
/--
`repeat { t }` applies `t` to each goal. If the application succeeds,
@ -920,7 +899,7 @@ If `h` is omitted, the name `this` is used.
-/
meta def «have» (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
let h := h.get_or_else `this in
match q₁, q₂ with
(match q₁, q₂ with
| some e, some p := do
t ← i_to_expr e,
v ← i_to_expr ``(%%p : %%t),
@ -932,8 +911,8 @@ match q₁, q₂ with
| none, none := do
u ← mk_meta_univ,
e ← mk_meta_var (sort u),
tactic.assert h e
end >> skip
tactic.assert h e)
>> skip
/--
`let h : t := p` adds the hypothesis `h : t := p` to the current goal if `p` a term of type `t`. If `t` is omitted, it will be inferred.
@ -944,20 +923,20 @@ If `h` is omitted, the name `this` is used.
-/
meta def «let» (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
let h := h.get_or_else `this in
match q₁, q₂ with
| some e, some p := do
t ← i_to_expr e,
v ← i_to_expr ``(%%p : %%t),
tactic.definev h t v
| none, some p := do
p ← i_to_expr p,
tactic.pose h none p
| some e, none := i_to_expr e >>= tactic.define h
| none, none := do
u ← mk_meta_univ,
e ← mk_meta_var (sort u),
tactic.define h e
end >> skip
(match q₁, q₂ with
| some e, some p := do
t ← i_to_expr e,
v ← i_to_expr ``(%%p : %%t),
tactic.definev h t v
| none, some p := do
p ← i_to_expr p,
tactic.pose h none p
| some e, none := i_to_expr e >>= tactic.define h
| none, none := do
u ← mk_meta_univ,
e ← mk_meta_var (sort u),
tactic.define h e)
>> skip
/--
`suffices h : t` is the same as `have h : t, tactic.swap`. In other words, it adds the hypothesis `h : t` to the current goal and opens a new subgoal with target `t`.
@ -1080,7 +1059,6 @@ private meta def resolve_exception_ids (all_hyps : bool) : list name → list na
| local_const n _ _ _ := when (not all_hyps) (fail $ sformat! "invalid local exception {id}, '*' was not used") >>
resolve_exception_ids ids gex (n::hex)
| _ := fail $ sformat! "invalid exception {id}, unknown identifier"
end
/- Return (hs, gex, hex, all) -/
meta def decode_simp_arg_list (hs : list simp_arg_type) : tactic $ list pexpr × list name × list name × bool :=
@ -1090,8 +1068,7 @@ do
match r, h with
| (es, ex, all), simp_arg_type.all_hyps := (es, ex, tt)
| (es, ex, all), simp_arg_type.except id := (es, id::ex, all)
| (es, ex, all), simp_arg_type.expr e := (e::es, ex, all)
end)
| (es, ex, all), simp_arg_type.expr e := (e::es, ex, all))
([], [], ff),
(gex, hex) ← resolve_exception_ids all ex [] [],
return (hs.reverse, gex, hex, all)
@ -1110,7 +1087,6 @@ when p.is_choice_macro $
fail $ to_fmt "ambiguous overload, possible interpretations" ++
format.join (ps.map (λ p, (to_fmt p).indent 4))
| _ := failed
end
private meta def simp_lemmas.resolve_and_add (s : simp_lemmas) (u : list name) (n : name) (ref : pexpr) : tactic (simp_lemmas × list name) :=
do
@ -1131,14 +1107,12 @@ do
(do e ← i_to_expr_no_subgoals p, b ← is_valid_simp_lemma e, guard b, try (save_type_info e ref), s ← s.add e, return (s, u))
<|>
report_invalid_simp_lemma n
end
private meta def simp_lemmas.add_pexpr (s : simp_lemmas) (u : list name) (p : pexpr) : tactic (simp_lemmas × list name) :=
match p with
| (const c []) := simp_lemmas.resolve_and_add s u c p
| (local_const c _ _ _) := simp_lemmas.resolve_and_add s u c p
| _ := do new_e ← i_to_expr_no_subgoals p, s ← s.add new_e, return (s, u)
end
private meta def simp_lemmas.append_pexprs : simp_lemmas → list name → list pexpr → tactic (simp_lemmas × list name)
| s u [] := return (s, u)
@ -1181,14 +1155,13 @@ do to_remove ← hs.mfilter $ λ h, do {
meta def simp_core (cfg : simp_config) (discharger : tactic unit)
(no_dflt : bool) (hs : list simp_arg_type) (attr_names : list name)
(locat : loc) : tactic unit :=
match locat with
| loc.wildcard := do (all_hyps, s, u) ← mk_simp_set_core no_dflt attr_names hs tt,
if all_hyps then tactic.simp_all s u cfg discharger
else do hyps ← non_dep_prop_hyps, simp_core_aux cfg discharger s u hyps tt
| _ := do (s, u) ← mk_simp_set no_dflt attr_names hs,
ns ← locat.get_locals,
simp_core_aux cfg discharger s u ns locat.include_goal
end
(match locat with
| loc.wildcard := do (all_hyps, s, u) ← mk_simp_set_core no_dflt attr_names hs tt,
if all_hyps then tactic.simp_all s u cfg discharger
else do hyps ← non_dep_prop_hyps, simp_core_aux cfg discharger s u hyps tt
| _ := do (s, u) ← mk_simp_set no_dflt attr_names hs,
ns ← locat.get_locals,
simp_core_aux cfg discharger s u ns locat.include_goal)
>> try tactic.triv >> try (tactic.reflexivity reducible)
/--
@ -1257,7 +1230,6 @@ match l with
dsimp_target s u {zeta := ff ..cfg},
intron n
| _ := l.apply (λ h, dsimp_hyp h s u cfg) (dsimp_target s u cfg)
end
/--
This tactic applies to a goal whose target has the form `t ~ u` where `~` is a reflexive relation, that is, a relation which has a reflexivity lemma tagged with the attribute `[refl]`. The tactic checks whether `t` and `u` are definitionally equal and then solves the goal.
@ -1288,7 +1260,6 @@ tactic.transitivity >> match q with
| some q :=
do (r, lhs, rhs) ← target_lhs_rhs,
i_to_expr q >>= unify rhs
end
/--
Given hypothesis `h : x = t` or `h : t = x`, where `x` is a local constant, `subst h` substitutes `x` by `t` everywhere in the main goal and then clears `h`.
@ -1338,7 +1309,6 @@ match l with
dunfold_target new_cs cfg,
intron n
| _ := do new_cs ← to_qualified_names cs, l.apply (λ h, dunfold_hyp cs h cfg) (dunfold_target new_cs cfg)
end
private meta def delta_hyps : list name → list name → tactic unit
| cs [] := skip
@ -1370,7 +1340,6 @@ match l with
| _ :=
l.try_apply (λ h, unfold_projs_hyp h cfg)
(tactic.unfold_projs_target cfg) <|> fail "unfold_projs failed to simplify"
end
end interactive

4
library/init/meta/interactive_base.lean
View file

@ -35,8 +35,8 @@ meta def loc.get_locals : loc → tactic (list expr)
| loc.wildcard := tactic.local_context
| (loc.ns xs) := xs.mfoldl (λ ls n, match n with
| none := pure ls
| some n := do l ← tactic.get_local n, pure $ l :: ls
end) []
| some n := do l ← tactic.get_local n, pure $ l :: ls)
[]
meta def loc.apply (hyp_tac : expr → tactic unit) (goal_tac : tactic unit) (l : loc) : tactic unit :=
do hs ← l.get_locals,

2
library/init/meta/rb_map.lean
View file

@ -121,7 +121,6 @@ meta def insert {key : Type} {data : Type} (rbl : rb_lmap key data) (k : key) (d
match (rb_map.find rbl k) with
| none := rb_map.insert rbl k [d]
| (some l) := rb_map.insert (rb_map.erase rbl k) k (d :: l)
end
meta def erase {key : Type} {data : Type} (rbl : rb_lmap key data) (k : key) :
rb_lmap key data :=
@ -134,7 +133,6 @@ meta def find {key : Type} {data : Type} (rbl : rb_lmap key data) (k : key) : li
match (rb_map.find rbl k) with
| none := []
| (some l) := l
end
end rb_lmap

3
library/init/meta/rec_util.lean
View file

@ -58,7 +58,7 @@ private meta def mk_constructors_arg_names_aux : list name → name → nat →
| [] p i r := return (list.reverse r)
| (c::cs) p i r := do
v : list name × nat ← mk_constructor_arg_names c p i,
match v with (l, i') := mk_constructors_arg_names_aux cs p i' (l :: r) end
match v with (l, i') := mk_constructors_arg_names_aux cs p i' (l :: r)
/-- Given an inductive datatype I with k constructors and where constructor i has n_i fields,
return the list [[p.1, ..., p.n_1], [p.{n_1 + 1}, ..., p.{n_1 + n_2}], ..., [..., p.{n_1 + ... + n_k}]] -/
@ -99,7 +99,6 @@ private meta def mk_constructor_fresh_names_aux : nat → expr → name_set →
mk_constructor_fresh_names_aux (nparams - 1) ty' s
}
| _ := return ([], s)
end
meta def mk_constructor_fresh_names (nparams : nat) (c : name) (s : name_set) : tactic (list name × name_set) :=
do d ← get_decl c,

1
library/init/meta/relation_tactics.lean
View file

@ -16,7 +16,6 @@ do tgt ← target >>= instantiate_mvars,
match (op_for env (const_name r)) with
| (some refl) := do r ← mk_const refl, apply_core r {md := md, new_goals := new_goals.non_dep_only} >> return ()
| none := fail $ tac_name ++ " tactic failed, target is not a relation application with the expected property."
end
meta def reflexivity (md := semireducible) : tactic unit :=
relation_tactic md environment.refl_for "reflexivity"

20
library/init/meta/simp_tactic.lean
View file

@ -53,15 +53,14 @@ namespace tactic
meta def revert_and_transform (transform : expr → tactic expr) (h : expr) : tactic unit :=
do num_reverted : ℕ ← revert h,
t ← target,
match t with
| expr.pi n bi d b :=
do h_simp ← transform d,
unsafe_change $ expr.pi n bi h_simp b
| expr.elet n g e f :=
do h_simp ← transform g,
unsafe_change $ expr.elet n h_simp e f
| _ := fail "reverting hypothesis created neither a pi nor an elet expr (unreachable?)"
end,
(match t with
| expr.pi n bi d b :=
do h_simp ← transform d,
unsafe_change $ expr.pi n bi h_simp b
| expr.elet n g e f :=
do h_simp ← transform g,
unsafe_change $ expr.elet n h_simp e f
| _ := fail "reverting hypothesis created neither a pi nor an elet expr (unreachable?)"),
intron num_reverted
/-- `get_eqn_lemmas_for deps d` returns the automatically generated equational lemmas for definition d.
@ -274,7 +273,7 @@ meta constant ext_simplify_core
private meta def is_equation : expr → bool
| (expr.pi n bi d b) := is_equation b
| e := match (expr.is_eq e) with (some a) := tt | none := ff end
| e := match (expr.is_eq e) with | (some a) := tt | none := ff
meta def collect_ctx_simps : tactic (list expr) :=
local_context
@ -447,7 +446,6 @@ es.mmap' $ λ e,
| some pr :=
assert e.h.local_pp_name e.new_type >>
mk_eq_mp pr e.h >>= exact
end
private meta def clear_old_hyps (es : list simp_all_entry) : tactic unit :=
es.mmap' $ λ e, when (e.pr ≠ none) (try (clear e.h))

30
library/init/meta/tactic.lean
View file

@ -65,13 +65,11 @@ meta def {u₁ u₂} tactic.up {α : Type u₂} (t : tactic α) : tactic (ulift.
λ s, match t s with
| success a s' := success (ulift.up a) s'
| exception t ref s := exception t ref s
end
meta def {u₁ u₂} tactic.down {α : Type u₂} (t : tactic (ulift.{u₁} α)) : tactic α :=
λ s, match t s with
| success (ulift.up a) s' := success a s'
| exception t ref s := exception t ref s
end
namespace tactic
variables {α : Type u}
@ -96,8 +94,6 @@ meta def try_lst : list (tactic unit) → tactic unit
match try_lst tacs s' with
| result.exception _ _ _ := result.exception e p s'
| r := r
end
end
meta def fail_if_success {α : Type u} (t : tactic α) : tactic unit :=
λ s, result.cases_on (t s)
@ -109,7 +105,6 @@ meta def success_if_fail {α : Type u} (t : tactic α) : tactic unit :=
| (interaction_monad.result.exception _ _ s') := success () s
| (interaction_monad.result.success a s) :=
mk_exception "success_if_fail combinator failed, given tactic succeeded" none s
end
open nat
/-- (iterate_at_most n t): repeat the given tactic at most n times or until t fails -/
@ -129,7 +124,6 @@ meta def returnopt (e : option α) : tactic α :=
λ s, match e with
| (some a) := success a s
| none := mk_exception "failed" none s
end
meta instance opt_to_tac : has_coe (option α) (tactic α) :=
⟨returnopt⟩
@ -141,8 +135,7 @@ meta def decorate_ex (msg : format) (t : tactic α) : tactic α :=
(λ opt_thunk,
match opt_thunk with
| some e := exception (some (λ u, msg ++ format.nest 2 (format.line ++ e u)))
| none := exception none
end)
| none := exception none)
@[inline] meta def write (s' : tactic_state) : tactic unit :=
λ s, success () s'
@ -169,8 +162,6 @@ meta def returnex {α : Type} (e : exceptional α) : tactic α :=
match get_options s with
| success opt _ := exception (some (λ u, f opt)) none s
| exception _ _ _ := exception (some (λ u, f options.mk)) none s
end
end
meta instance ex_to_tac {α : Type} : has_coe (exceptional α) (tactic α) :=
⟨returnex⟩
@ -594,7 +585,6 @@ match t with
| expr.pi _ _ _ _ := do H ← intro1, Hs ← intros, return (H :: Hs)
| expr.elet _ _ _ _ := do H ← intro1, Hs ← intros, return (H :: Hs)
| _ := return []
end
meta def intro_lst : list name → tactic (list expr)
| [] := return []
@ -613,7 +603,6 @@ do t ← target,
| expr.pi _ _ _ b := proc b
| expr.elet _ _ _ b := proc b
| _ := return []
end
meta def introv : list name → tactic (list expr)
| [] := intros_dep
@ -642,7 +631,6 @@ do lctx ← local_context,
| some [] := revert_lst lctx
/- `hi` is the last local instance. We shoul truncate `lctx` at `hi`. -/
| some (hi::his) := revert_lst $ lctx.foldl (λ r h, if h.local_uniq_name = hi.local_uniq_name then [] else h :: r) []
end
meta def clear_lst : list name → tactic unit
| [] := skip
@ -652,50 +640,42 @@ meta def match_not (e : expr) : tactic expr :=
match (expr.is_not e) with
| (some a) := return a
| none := fail "expression is not a negation"
end
meta def match_and (e : expr) : tactic (expr × expr) :=
match (expr.is_and e) with
| (some (α, β)) := return (α, β)
| none := fail "expression is not a conjunction"
end
meta def match_or (e : expr) : tactic (expr × expr) :=
match (expr.is_or e) with
| (some (α, β)) := return (α, β)
| none := fail "expression is not a disjunction"
end
meta def match_iff (e : expr) : tactic (expr × expr) :=
match (expr.is_iff e) with
| (some (lhs, rhs)) := return (lhs, rhs)
| none := fail "expression is not an iff"
end
meta def match_eq (e : expr) : tactic (expr × expr) :=
match (expr.is_eq e) with
| (some (lhs, rhs)) := return (lhs, rhs)
| none := fail "expression is not an equality"
end
meta def match_ne (e : expr) : tactic (expr × expr) :=
match (expr.is_ne e) with
| (some (lhs, rhs)) := return (lhs, rhs)
| none := fail "expression is not a disequality"
end
meta def match_heq (e : expr) : tactic (expr × expr × expr × expr) :=
do match (expr.is_heq e) with
| (some (α, lhs, β, rhs)) := return (α, lhs, β, rhs)
| none := fail "expression is not a heterogeneous equality"
end
meta def match_refl_app (e : expr) : tactic (name × expr × expr) :=
do env ← get_env,
match (environment.is_refl_app env e) with
| (some (R, lhs, rhs)) := return (R, lhs, rhs)
| none := fail "expression is not an application of a reflexive relation"
end
meta def match_app_of (e : expr) (n : name) : tactic (list expr) :=
guard (expr.is_app_of e n) >> return e.get_app_args
@ -745,7 +725,6 @@ do gs ← get_goals,
match gs with
| (g₁ :: g₂ :: rs) := set_goals (g₂ :: g₁ :: rs)
| e := skip
end
/-- `assert h t`, adds a new goal for t, and the hypothesis `h : t` in the current goal. -/
meta def assert (h : name) (t : expr) : tactic expr :=
@ -797,7 +776,6 @@ private meta def repeat_aux (t : tactic unit) : list expr → list expr → tact
| _ := do
gs' ← get_goals,
repeat_aux (gs' ++ gs) r
end
/-- This tactic is applied to each goal. If the application succeeds,
the tactic is applied recursively to all the generated subgoals until it eventually fails.
@ -824,8 +802,6 @@ do gs ← get_goals,
match gs' with
| [] := set_goals rs
| gs := fail "solve1 tactic failed, focused goal has not been solved"
end
end
/-- `solve [t_1, ... t_n]` applies the first tactic that solves the main goal. -/
meta def solve (ts : list (tactic unit)) : tactic unit :=
@ -856,7 +832,6 @@ do g::gs ← get_goals,
gs' ← get_goals,
set_goals (gs' ++ gs),
return a
end
private meta def all_goals_core (tac : tactic unit) : list expr → list expr → tactic unit
| [] ac := set_goals ac
@ -1074,7 +1049,6 @@ do tgt : expr ← target,
match H with
| some n := intro n
| none := intro1
end
private meta def generalizes_aux (md : transparency) : list expr → tactic unit
| [] := skip
@ -1208,7 +1182,6 @@ meta def try_for {α} (max : nat) (tac : tactic α) : tactic α :=
match _root_.try_for max (tac s) with
| some r := r
| none := mk_exception "try_for tactic failed, timeout" none s
end
meta def updateex_env (f : environment → exceptional environment) : tactic unit :=
do env ← get_env,
@ -1288,7 +1261,6 @@ meta def any_of {α β} : list α → (α → tactic β) → tactic β
match opt_b with
| some b := return b
| none := any_of es fn
end
end list
/- Install monad laws tactic and use it to prove some instances. -/

1
library/system/io.lean
View file

@ -52,7 +52,6 @@ cleanup,
match res with
| sum.inr res := return res
| sum.inl error := monad_io.fail _ _ _ error
end
protected def fail {α : Type} (s : string) : io α :=
monad_io.fail io_core _ _ (io.error.other s)

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

@ -81,10 +81,6 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
consume_until_end_or_command(p);
ex.rethrow();
}
if (p.curr_is_token(get_end_tk())) {
// TODO(Sebastian): legacy syntax, remove
p.next();
}
expr f = p.save_pos(mk_equations(header, eqns.size(), eqns.data()), pos);
return p.mk_app(f, ts, pos);
}

11
tests/lean/parser1.lean
View file

@ -5,19 +5,16 @@ def test {α} [decidable_eq α] (p : parser α) (s : string) (e : α) : io unit
match parse p s with
| except.ok a := if a = e then return () else io.print_ln "unexpected result"
| except.error e := io.print_ln (e.to_string s)
end
def test_failure {α} (p : parser α) (s : string) : io unit :=
match parse p s with
| except.ok a := io.print_ln "unexpected success"
| except.error e := return ()
end
def show_result {α} [has_to_string α] (p : parser α) (s : string) : io unit :=
match parse p s with
| except.ok a := io.print_ln "result: " >> io.print_ln (repr $ to_string a)
| except.error e := io.print_ln (e.to_string s)
end
#eval test (ch 'a') "a" 'a'
#eval test any "a" 'a'
@ -149,12 +146,10 @@ instance eq_expr : decidable_eq Expr
| (Add e₁ e₂) (Var y) := is_false (λ h, Expr.no_confusion h)
| (Add e₁ e₂) (Add e₃ e₄) :=
match eq_expr e₁ e₃ with
| is_true h := match eq_expr e₂ e₄ with
| is_true h' := is_true (h ▸ h' ▸ rfl)
| is_false h' := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₂ h'))
end
| is_true h := (match eq_expr e₂ e₄ with
| is_true h' := is_true (h ▸ h' ▸ rfl)
| is_false h' := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₂ h')))
| is_false h := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₁ h))
end
def parse_atom (p : parser Expr) : parser Expr :=
(Var <$> lexeme var <?> "variable")

1
tests/lean/run/parser_ir1.lean
View file

@ -8,7 +8,6 @@ def show_result {α} [lean.has_to_format α] (p : parser α) (s : string) : io u
match parse p s with
| except.ok a := io.print_ln (lean.to_fmt a)
| except.error e := io.print_ln (e.to_string s)
end
def IR := "
def succ (x : uint32) : uint32 :=

2
tests/lean/trust0/basic.lean
View file

@ -49,7 +49,6 @@ instance : decidable_eq ℕ
match decidable_eq x y with
| is_true xeqy := is_true (xeqy ▸ eq.refl (succ x))
| is_false xney := is_false (λ h, nat.no_confusion h (λ xeqy, absurd xeqy xney))
end
def {u} repeat {α : Type u} (f : ℕ → α → α) : ℕ → α → α
| 0 a := a
@ -98,7 +97,6 @@ instance decidable_le : ∀ a b : ℕ, decidable (a ≤ b)
match decidable_le a b with
| is_true h := is_true (succ_le_succ h)
| is_false h := is_false (λ a, h (le_of_succ_le_succ a))
end
instance decidable_lt : ∀ a b : ℕ, decidable (a < b) :=
λ a b, nat.decidable_le (succ a) b