Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Removed the XIH rule.

  • Loading branch information...
commit e61dfc5f29468b017963806808554e493273bb49 1 parent ab06f38
@luqui authored
Showing with 3 additions and 22 deletions.
  1. +1 −7 ixi/IXi/Proof.hs
  2. +1 −8 ixi/IXi/Sequent.hs
  3. +1 −7 ixi/IXi/Tactic.hs
View
8 ixi/IXi/Proof.hs
@@ -1,7 +1,7 @@
module IXi.Proof
( Proof
, hypothesis, conversion
- , implRule, xiRule, hxiRule, hhRule, xihRule
+ , implRule, xiRule, hxiRule, hhRule
, theorem
, Theorem, thmStatement, thmProof, prove
)
@@ -20,7 +20,6 @@ data Proof
| XiRule Name Proof Proof
| HXiRule Name Proof Proof
| HHRule
- | XIHRule Proof
| Theorem Theorem
deriving (Show)
@@ -30,7 +29,6 @@ implRule = ImplRule
xiRule = XiRule
hxiRule = HXiRule
hhRule = HHRule
-xihRule = XIHRule
theorem = Theorem
@@ -57,10 +55,6 @@ checkProof (HXiRule name hproof hxiproof) seq = do
checkProof HHRule seq = S.hhRule seq
-checkProof (XIHRule pf) seq = do
- seq' <- S.xihRule seq
- checkProof pf seq'
-
checkProof (Theorem (MkTheorem t _)) (hyps S.:|- goal)
| goal == t = Right ()
| otherwise = Left "Goal does not match theorem"
View
9 ixi/IXi/Sequent.hs
@@ -3,7 +3,7 @@ module IXi.Sequent
, goal, hypotheses
, Err
, hypothesis, conversion, implRule
- , xiRule, hxiRule, hhRule, xihRule
+ , xiRule, hxiRule, hhRule
, newName
)
where
@@ -70,10 +70,3 @@ hhRule (hyps :|- goal) = invalid goal "Goal is not an H-H-form"
newName :: Sequent -> Name
newName seq = safeName' (goal seq : hypotheses seq)
-
--- conservative extension, Γ,x |- Hx
-xihRule :: Sequent -> Err Sequent
-xihRule (hyps :|- goal) =
- case goal of
- H :% x -> valid (hyps :|- x)
- _ -> invalid goal "Goal is not an H-form"
View
8 ixi/IXi/Tactic.hs
@@ -1,6 +1,6 @@
module IXi.Tactic
( Tactic, Hypothesis
- , conversion, implRule, xiRule, hxiRule, hhRule, xihRule, theorem
+ , conversion, implRule, xiRule, hxiRule, hhRule, theorem
, inspect, (>|<)
, newName, failure
, prove
@@ -57,12 +57,6 @@ hhRule = Tactic $ \seq -> do
() <- Seq.hhRule seq
return P.hhRule
-xihRule :: Hypothesis -> Tactic
-xihRule tac = Tactic $ \seq -> do
- seq' <- Seq.xihRule seq
- pf <- unTactic tac seq'
- return (P.xihRule pf)
-
theorem :: P.Theorem -> Tactic
theorem thm = Tactic $ \seq -> do
if P.thmStatement thm == Seq.goal seq
Please sign in to comment.
Something went wrong with that request. Please try again.