Ensure metavariables aren't re-used in rules and queries
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
f4619672a9
commit
1e12dc8032
|
@ -152,7 +152,7 @@ proveTerm t =
|
||||||
|
|
||||||
prove : Term Metavariable -> Prover ProofTree
|
prove : Term Metavariable -> Prover ProofTree
|
||||||
prove mt =
|
prove mt =
|
||||||
liftInstantiation instantiate mt
|
withVars (liftInstantiation instantiate mt)
|
||||||
|> andThen proveTerm
|
|> andThen proveTerm
|
||||||
|
|
||||||
single : RuleEnv -> Prover a -> Maybe a
|
single : RuleEnv -> Prover a -> Maybe a
|
||||||
|
|
Loading…
Reference in New Issue
Block a user