diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/lean.ml')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/lean.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/lean.ml b/rego-proofs/compiler-rewrite/lib/lean.ml index f43c5c3..41abee3 100644 --- a/rego-proofs/compiler-rewrite/lib/lean.ml +++ b/rego-proofs/compiler-rewrite/lib/lean.ml @@ -10,7 +10,7 @@ type lean_expression = | Tuple of lean_expression list | Application of lean_expression * lean_expression list | Define of string * lean_expression - | Inductive of string * judgement list * (string * lean_expression * lean_expression list) list + | Inductive of string * judgement list * (string * lean_expression list * lean_expression list) list | ForAll of judgement * lean_expression | Exists of judgement * lean_expression @@ -41,14 +41,18 @@ let rec fmt_lean_expression : lean_expression -> string = function | Exists (j, expr) -> Printf.sprintf "∃ %s, %s" (fmt_judgement j) (fmt_lean_expression expr) | Inductive (name, judgements, arms) -> - let fmt_arm (arm_name, expr, values) = + let fmt_arm (arm_name, exprs, values) = let head = Printf.sprintf "%s %s" name (List.map ~f:fmt_lean_expression values |> String.concat ~sep:" ") in - Printf.sprintf " | %s : %s → %s" arm_name (fmt_lean_expression expr) head + let body = + List.map ~f:fmt_lean_expression exprs + |> String.concat ~sep:" → " + in + Printf.sprintf " | %s : %s → %s" arm_name body head in Printf.sprintf "inductive %s %s where\n%s" name (List.map ~f:fmt_judgement judgements |> String.concat ~sep:" ") |