diff options
| author | Jakob L. Kreuze | 2023-10-31 14:02:55 -0400 |
|---|---|---|
| committer | Jakob L. Kreuze | 2023-10-31 14:02:55 -0400 |
| commit | 55b391229361435e3f29fefab82c738316d63ec4 (patch) | |
| tree | e262d91e8393612c6cde54bf028a7affafd3abc3 /rego-proofs/compiler-rewrite/lib/compiler.mli | |
| parent | b65d0fd86ca4a94364d16968b87729986967eb5c (diff) | |
More detailed variable usage analysis
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 |