Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
cdotTuple.lean
blob: 5b15e85f3f739fc2a64e6301f8e769b56914b55b [
file
] [
edit
]
#eval [1, 2, 3].map (·, 1)
#eval (·, ·) 1 2
#eval (·, ·, ·) 1 2 3
theorem ex1
:
[
1
,
2
,
3
].
map
(·,
1
)
=
[(
1
,
1
),
(
2
,
1
),
(
3
,
1
)]
:=
rfl
theorem ex2
:
(·,
·)
1
2
=
(
1
,
2
)
:=
rfl