From 89131ba1fff10eb0967bd07ed8aec4aff070fa90 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 16 Jul 2017 23:34:50 +0100 Subject: [PATCH] feat(init/meta/interactive): expose custom hyp name in by_contra --- library/init/meta/interactive.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 91eb90815c..56a8484d41 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -1023,11 +1023,11 @@ meta def by_cases (q : parse texpr) (n : parse (tk "with" *> ident)?): tactic un do p ← tactic.to_expr_strict q, tactic.by_cases p (n.get_or_else `h) -meta def by_contradiction : tactic unit := -tactic.by_contradiction >> return () +meta def by_contradiction (n : parse ident?) : tactic unit := +tactic.by_contradiction n >> return () -meta def by_contra : tactic unit := -tactic.by_contradiction >> return () +meta def by_contra (n : parse ident?) : tactic unit := +tactic.by_contradiction n >> return () /-- Type check the given expression, and trace its type. -/ meta def type_check (p : parse texpr) : tactic unit :=