15 lines
272 B
Text
15 lines
272 B
Text
data Bool () where
|
|
True : Bool ()
|
|
False : Bool ()
|
|
|
|
-- Both valid
|
|
-- f : Bool () -> a -> Int
|
|
f : Bool () -> (forall a. a -> Int)
|
|
f b = case b of
|
|
False => (\x. 0 : forall a. a -> Int)
|
|
True => (\x. 1 : forall a. a -> Int)
|
|
|
|
|
|
main : Int
|
|
main = (f True) 'h'
|
|
|