diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/lean.mli')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/lean.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/lean.mli b/rego-proofs/compiler-rewrite/lib/lean.mli index 1626dfa..990ab5f 100644 --- a/rego-proofs/compiler-rewrite/lib/lean.mli +++ b/rego-proofs/compiler-rewrite/lib/lean.mli @@ -8,7 +8,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 |