blob: 990ab5f6368854b6ac45fc0dc7b8bb96f1ffa2cb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
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
and judgement = string list * string
val fmt_lean_expression : lean_expression -> string
|
© 2015 - 2026 Jakob L. Kreuze
