Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/cancelparams
/
.
/
tests
/
lean
/
unexpandersNamespaces.lean
blob: 14e23a23aaef3b3b0c3ccfb5f4fef9b71b796560 [
file
] [
edit
]
namespace
Foo
abbrev
List
(α
:
Type
u
)
:
Type
:=
Unit
def
List
.
nil
{α
:
Type
u
}
:
List
α
:=
()
def
List
.
cons
{α
:
Type
u
}
(
x
:
α)
(
xs
:
List
α)
:
List
α
:=
()
#check @List.nil Unit
#check @_root_.List.nil Unit
end
Foo