diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/lean.ml')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/lean.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/lean.ml b/rego-proofs/compiler-rewrite/lib/lean.ml index 41abee3..b3526e3 100644 --- a/rego-proofs/compiler-rewrite/lib/lean.ml +++ b/rego-proofs/compiler-rewrite/lib/lean.ml @@ -13,8 +13,9 @@ type lean_expression = | Inductive of string * judgement list * (string * lean_expression list * lean_expression list) list | ForAll of judgement * lean_expression | Exists of judgement * lean_expression +[@@deriving eq, show] -and judgement = string list * string +and judgement = string list * string [@@deriving eq, show] let fmt_judgement : judgement -> string = function | vars, t -> Printf.sprintf "(%s : %s)" (String.concat ~sep:" " vars) t |