Documentation
Std
.
Lean
.
Except
Search
Google site search
return to top
source
Imports
Init
Lean.Util.Trace
Imported by
Except
.
emoji
source
def
Except
.
emoji
{ε :
Type
u_1}
{α :
Type
u_2}
:
Except
ε
α
→
String
Visualize an
Except
using a checkmark or a cross.
Equations
Except.emoji
x
=
match
x
with |
Except.error
a
=>
Lean.crossEmoji
|
Except.ok
a
=>
Lean.checkEmoji
Instances For