Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/Array.mapIdx
/
.
/
tests
/
lean
/
2505.lean.expected.out
blob: 98a7adec30c0fa844ead2f557dccde2747c5d7b3 [
file
] [
edit
]
2505.lean
:
14
:
0
-
14
:
7
:
warning
:
declaration uses
'sorry'
target
:
A
(
OfNat
.
ofNat
.{
0
}
Nat
1
(
instOfNatNat
1
))
target
' : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
