rego-proofs/compiler-rewrite/lib/compiler.mli


1
2
3
4
5
6
7
8
9
10
11
12
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