summaryrefslogtreecommitdiff
path: root/Command.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Command.hs')
-rw-r--r--Command.hs8
1 files changed, 4 insertions, 4 deletions
diff --git a/Command.hs b/Command.hs
index 6df88f8..e6e0e39 100644
--- a/Command.hs
+++ b/Command.hs
@@ -173,11 +173,11 @@ refl term =
Theorem Set.empty (mkEquals term term)
-subst :: Theorem -> [Object] -> Theorem
+subst :: Theorem -> [Object] -> Maybe Theorem
subst thm list =
- let s = makeSubst list
- in Theorem (Set.map (substitute s) (thmHyp thm))
- (substitute s (thmCon thm))
+ do s <- makeSubst list
+ return (Theorem (Set.map (substitute s) (thmHyp thm))
+ (substitute s (thmCon thm)))
thm :: Term -> [Term] -> Theorem -> Maybe Theorem