chore(tactic/monotonicity/interactive) use derive for has_reflect

leanprover-community · Jan 8, 2019 · 1eb4814 · 1eb4814
1 parent 2e63635
commit 1eb4814
Showing 1 changed file with 2 additions and 6 deletions.
diff --git a/tactic/monotonicity/interactive.lean b/tactic/monotonicity/interactive.lean
@@ -546,14 +546,10 @@ meta def repeat_until_or_at_most : nat → tactic unit → tactic unit → tacti
 meta def repeat_until : tactic unit → tactic unit → tactic unit :=
 repeat_until_or_at_most 100000
 
-inductive rep_arity
+@[derive _root_.has_reflect]
+inductive rep_arity : Type
 | one | exactly (n : ℕ) | many
 
-meta instance has_reflect_rep_arity : has_reflect rep_arity
- | rep_arity.one := `(_)
- | rep_arity.many := `(_)
- | (rep_arity.exactly n) := `(_)
-
 meta def repeat_or_not : rep_arity → tactic unit → option (tactic unit) → tactic unit
  | rep_arity.one  tac none := tac
  | rep_arity.many tac none := repeat tac