@@ -376,7 +376,7 @@ newtype instance Goal.Rule Goal =
376
376
deriving (Eq , GHC.Generic , Show )
377
377
378
378
instance Goal. Goal Goal where
379
- strategy _ goals rules =
379
+ strategy _ _ _ =
380
380
firstStep :> Stream. iterate id nextStep
381
381
where
382
382
firstStep =
@@ -385,7 +385,7 @@ instance Goal.Goal Goal where
385
385
, ProofState. CheckGoalRemainder
386
386
, ProofState. CheckImplication
387
387
, ProofState. TriviallyValid
388
- , ProofState. DerivePar axioms
388
+ , ProofState. ApplyAxioms
389
389
, ProofState. Simplify
390
390
, ProofState. TriviallyValid
391
391
, ProofState. ResetGoal
@@ -397,19 +397,17 @@ instance Goal.Goal Goal where
397
397
, ProofState. CheckGoalRemainder
398
398
, ProofState. CheckImplication
399
399
, ProofState. TriviallyValid
400
- , ProofState. DeriveSeq claims
400
+ , ProofState. ApplyClaims
401
401
, ProofState. CheckImplication
402
402
, ProofState. Simplify
403
403
, ProofState. TriviallyValid
404
- , ProofState. DerivePar axioms
404
+ , ProofState. ApplyAxioms
405
405
, ProofState. CheckImplication
406
406
, ProofState. Simplify
407
407
, ProofState. TriviallyValid
408
408
, ProofState. ResetGoal
409
409
, ProofState. TriviallyValid
410
410
]
411
- axioms = rules
412
- claims = Rule <$> goals
413
411
414
412
checkImplication (src, dst) =
415
413
return . Goal. NotImplied $ (difference src dst, dst)
0 commit comments