diff options
Diffstat (limited to 'rego-proofs/compiler/lib/compiler.mli')
| -rw-r--r-- | rego-proofs/compiler/lib/compiler.mli | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/rego-proofs/compiler/lib/compiler.mli b/rego-proofs/compiler/lib/compiler.mli new file mode 100644 index 0000000..0bef961 --- /dev/null +++ b/rego-proofs/compiler/lib/compiler.mli @@ -0,0 +1,13 @@ +open Ast +open Lean + +type environ + +type analysis_result = + { bound : string list; + free : string list; + used : string list } + +val extract_variables_wrapper : query -> analysis_result +val transform_rule_with_ref_head : rule -> rule list +val compile_package : package -> lean_expression list |