Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/replace
/
.
/
tests
/
lean
/
classBadOutParam.lean
blob: 5f3b9c725049b778a9675a7ccf244bcf4e6d4135 [
file
] [
edit
]
class
C1
(
x
:
outParam
Nat
)
(
y
:
{
n
:
Nat
// n > x }) (α : Type) := -- should fail
(
val
:
α)
class
C2
(
x
:
outParam
Nat
)
(
y
:
outParam
{
n
:
Nat
// n > x }) (α : Type) := -- should work
(
val
:
α)