Deprecation warnings for match ⋯ with.
, fun.
, λ.
, and intro.
.
The syntax match ⋯ with.
has been deprecated in favor of nomatch ⋯
.
Both now support multiple discriminants.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The syntax fun.
has been deprecated in favor of nofun
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The syntax λ.
has been deprecated in favor of nofun
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The syntax match ⋯ with.
has been deprecated in favor of nomatch ⋯
.
Both now support multiple discriminants.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The syntax intro.
is deprecated in favor of nofun
.
Equations
- One or more equations did not get rendered due to their size.