Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
privateFieldCopyIssue.lean.out.expected
blob: 7f892bad56df7e6b737eecc906154327d9f3910e [
file
] [
edit
]
@[
reducible
]
protected
def
A
.
b
:
A
→
Nat
:=
fun
self
=>
self
.
2
@[
reducible
]
private
def
A
.
c
:
A
→
Nat
:=
fun
self
=>
self
.
3
@[
reducible
]
private
def
C
.
d
:
C
→
Nat
:=
fun
self
=>
self
.
2
@[
reducible
]
protected
def
C
.
e
:
C
→
Nat
:=
fun
self
=>
self
.
3