mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-16 15:52:43 +03:00
14 lines
175 B
Idris
14 lines
175 B
Idris
|
parameters (X : Nat)
|
||
|
Foo : Type
|
||
|
Foo = Nat
|
||
|
|
||
|
record Bar where
|
||
|
constructor MkBar
|
||
|
Gnu : Foo
|
||
|
|
||
|
Baz : Foo -> Nat
|
||
|
Baz x = x
|
||
|
|
||
|
Quux : Bar -> Foo
|
||
|
Quux x = Gnu x
|