Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/dead-cpp-removal
/
.
/
tests
/
compile
/
tuple.lean
blob: 5fd0be76a63b3d1c4e1163835d7420a43e5a9b59 [
file
] [
edit
]
@[
noinline
]
def
f
(
a
:
Nat
×
Nat
×
Nat
)
:
Nat
:=
a
.
fst
+
a
.
snd
.
fst
+
a
.
snd
.
snd
def
main
:
IO
Unit
:=
do
IO
.
println
(
f
(
1
,
2
,
3
,))