Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanLevelIMax  |
|
| | ||||
▪
The rule is what makes impredicative: a whose codomain is in (level ) stays in , regardless of the domain's level. Lean uses for the level of a dependent function type.
imax
Prop
∀
Prop
0
Prop
Examples
(1)
Basic Examples
(1)
Examples Initialization
The impredicative max of two universe parameters:
In[1]:=
 | LeanLevelIMax |
 | LeanLevelParam |
| LeanLevelParam |
Out[1]=
imax(u,v)
 |
|
 |
|
""