From b1c4527a28de4297e70f17c0cd496bbb8507031d Mon Sep 17 00:00:00 2001 From: "Adam C. Foltzer" Date: Wed, 20 Aug 2014 17:13:04 -0700 Subject: [PATCH] reference ticket in sat result documentation --- cryptol/REPL/Command.hs | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/cryptol/REPL/Command.hs b/cryptol/REPL/Command.hs index e3fc1197..61ee715d 100644 --- a/cryptol/REPL/Command.hs +++ b/cryptol/REPL/Command.hs @@ -352,18 +352,8 @@ proveCmd str = do bindItVariable t e -- | Run a SAT solver on the given expression. Binds the @it@ variable --- to a record whose form depends on the expression given. --- --- For unsatisfiable formulas: --- { result = False } --- --- For satisfiable formulas of the type @t -> Bit@: --- { result = True, arg = e } --- where e : t --- --- For satisfiable formulas of the type @t1 -> t2 -> ... -> Bit@: --- { result = True, arg = (e1, e2, ...) } --- where e1 : t1, e2 : t2, ... +-- to a record whose form depends on the expression given. See ticket +-- #66 for a discussion of this design. satCmd :: String -> REPL () satCmd str = do parseExpr <- replParseExpr str