Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
uintMatch.lean
blob: 8629d967082ac405d0fdf678621906f338063291 [
file
] [
edit
]
def
f
:
UInt8
→
Bool
|
5
=>
true
|
_
=>
false
#eval f 8
#eval f 5
def
g
:
UInt32
→
String
|
5
=>
"hello"
|
1555
=>
"world"
|
_
=>
"bla"
#eval g 5
#eval g 1555
#eval g 555