diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/compiler.mli')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.mli b/rego-proofs/compiler-rewrite/lib/compiler.mli index bdbc730..58a9c14 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.mli +++ b/rego-proofs/compiler-rewrite/lib/compiler.mli @@ -3,5 +3,10 @@ open Lean type environ -val extract_variables_wrapper : query -> (string list * string list) +type analysis_result = + { bound : string list; + free : string list; + used : string list } + +val extract_variables_wrapper : query -> analysis_result val compile_package : package -> lean_expression list |