fix(category/basic): change "try" to "mtry"

Author: digama0

category/applicative.lean

@@ -26,7 +26,7 @@ by simp [flip] with functor_norm
 
 lemma applicative.pure_seq_eq_map' (g : α → β) :
   (<*>) (pure g : f (α → β)) = (<$>) g :=
-by ext; simp with functor_norm
+by funext; simp with functor_norm
 
 end lemmas
 

category/basic.lean

@@ -85,7 +85,7 @@ variables {f : Type → Type v} [alternative f]
 
 def succeeds {α} (x : f α) : f bool := (x $> tt) <|> pure ff
 
-def try {α} (x : f α) : f unit := (x $> ()) <|> pure ()
+def mtry {α} (x : f α) : f unit := (x $> ()) <|> pure ()
 
 @[simp] theorem guard_true {h : decidable true} :
   @guard f _ true h = pure () := by simp [guard]

tactic/converter/old_conv.lean

@@ -192,8 +192,8 @@ meta def congr_core (c_f c_a : old_conv unit) : old_conv unit :=
   (expr.app f a) ← return lhs,
   f_type ← infer_type f >>= tactic.whnf,
   guard (f_type.is_arrow),
-  ⟨(), new_f, of⟩ ← try c_f r f,
-  ⟨(), new_a, oa⟩ ← try c_a r a,
+  ⟨(), new_f, of⟩ ← mtry c_f r f,
+  ⟨(), new_a, oa⟩ ← mtry c_a r a,
   rhs ← return $ new_f new_a,
   match of, oa with
   | none, none      :=