blob: f6a769a8a7b74493e44ff12b358563ee23918e27 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
type lean_expression =
| Comment of string
| Identifier of string
| Bool of bool
| String of string
| Number of float
| List of lean_expression list
| 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 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
val equal_lean_expression : lean_expression -> lean_expression -> bool
val equal_judgement : judgement -> judgement -> bool
val pp_lean_expression : Format.formatter -> lean_expression -> unit
val show_lean_expression : lean_expression -> string
val pp_judgement : Format.formatter -> judgement -> unit
val show_judgement : judgement -> string
val fmt_lean_expression : lean_expression -> string
|
© 2015 - 2026 Jakob L. Kreuze
