mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-16 20:03:27 +03:00
reference ticket in sat result documentation
This commit is contained in:
parent
1cf61e12c3
commit
b1c4527a28
@ -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
|
||||
|
Loading…
Reference in New Issue
Block a user