diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/lean.mli')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/lean.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/lean.mli b/rego-proofs/compiler-rewrite/lib/lean.mli index fb58c72..f6a769a 100644 --- a/rego-proofs/compiler-rewrite/lib/lean.mli +++ b/rego-proofs/compiler-rewrite/lib/lean.mli @@ -11,6 +11,7 @@ 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 + | ExistsUnique of judgement * lean_expression and judgement = string list * string |