Permalink
Browse files

Added "theorem" tactic.

  • Loading branch information...
1 parent c92d34c commit eaf863e6236e0ddf9998c4eb8576daf09cb83f3e @luqui committed Jun 11, 2009
Showing with 7 additions and 1 deletion.
  1. +7 −1 ixi/IXi/Tactic.hs
View
@@ -1,6 +1,6 @@
module IXi.Tactic
( Tactic, Hypothesis
- , hypothesis, conversion, implRule, xiRule, hxiRule, hhRule, xihRule
+ , hypothesis, conversion, implRule, xiRule, hxiRule, hhRule, xihRule, theorem
, inspect, (>|<)
, newName
)
@@ -63,6 +63,12 @@ xihRule (Hypothesis z) = Tactic $ \seq -> do
() <- Seq.xihRule ix seq
return (P.xihRule ix)
+theorem :: P.Theorem -> Tactic
+theorem thm = Tactic $ \seq -> do
+ if P.thmStatement thm == Seq.goal seq
+ then return (P.theorem thm)
+ else fail "Theorem does not match goal"
+
inspect :: (Seq.Sequent -> Tactic) -> Tactic
inspect f = Tactic $ \seq -> unTactic (f seq) seq

0 comments on commit eaf863e

Please sign in to comment.