From 01bc4dfcd2516de1185e989b0f7a09f308b700d4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Nov 2016 11:42:57 -0800 Subject: [PATCH] feat(library/init/meta/tactic): add dec_trivial notation --- library/init/meta/tactic.lean | 2 ++ tests/lean/run/find.lean | 2 -- tests/lean/run/size_of1.lean | 2 -- 3 files changed, 2 insertions(+), 4 deletions(-) diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index d6c8ca950e..709a6919e4 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -654,6 +654,8 @@ infer_type fn >>= get_pi_arity meta def triv : tactic unit := mk_const `trivial >>= exact +notation `dec_trivial` := of_as_true (by tactic.triv) + meta def by_contradiction (H : name) : tactic expr := do tgt : expr ← target, (match_not tgt >> return ()) diff --git a/tests/lean/run/find.lean b/tests/lean/run/find.lean index 39c998541b..d520a6b23f 100644 --- a/tests/lean/run/find.lean +++ b/tests/lean/run/find.lean @@ -1,6 +1,4 @@ open nat -notation `dec_trivial` := of_as_true (by tactic.triv) - lemma aux : ∃ x : nat, x > 10 := exists.intro 15 dec_trivial diff --git a/tests/lean/run/size_of1.lean b/tests/lean/run/size_of1.lean index 3601d3cf0c..454e12d6c0 100644 --- a/tests/lean/run/size_of1.lean +++ b/tests/lean/run/size_of1.lean @@ -1,7 +1,5 @@ open tactic -notation `dec_trivial` := of_as_true (by triv) - example : sizeof [tt, tt] < sizeof [tt, ff, tt] := dec_trivial