Induction proofs using variables & assumptions

1 files changed, 2 insertions, 0 deletions

diff --git a/Smurf.dcl b/Smurf.dcl
index 2c4fd1b..0ca45b2 100644
--- a/Smurf.dcl
+++ b/Smurf.dcl
@@ -66,6 +66,8 @@ instance toLaTeX DerivationTree
 step :: !Program State u:io u:(IO u:io) -> u:(Maybe (!Program, State), u:io)
 run :: !Program State io (IO io) -> (Maybe State, io)
 
+quotify :: Expr -> Expr
+
 listIO :: IO ListIO
 prover :: ((Program, Stack, State) -> Maybe (Stack, Stack, State))
 	Program State ListIO (IO ListIO) -> Maybe DerivationTree