Slightly tweak code for proving a term
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
da470f5caa
commit
aa7fd44a6d
|
@ -169,7 +169,8 @@ provePremises = mapM proveTerm
|
||||||
|
|
||||||
proveTerm : Term UnificationVar -> Prover ProofTree
|
proveTerm : Term UnificationVar -> Prover ProofTree
|
||||||
proveTerm t =
|
proveTerm t =
|
||||||
map (reify t) getUnificationState
|
getUnificationState
|
||||||
|
|> map (\us -> reify t us)
|
||||||
|> andThen (\tp ->
|
|> andThen (\tp ->
|
||||||
burn (
|
burn (
|
||||||
getRules
|
getRules
|
||||||
|
|
Loading…
Reference in New Issue
Block a user