module Test where {- typechecks -} t1 : Set -> Set -> Set t1 x = \z -> let y : Set y = x in y {- does not typecheck -} t2 : Set -> Set -> Set t2 x = let y : Set y = x in \z -> y
(Adga Version 2.1.2)
Fixed. -- Ulf
Page last modified on October 18, 2007, at 01:18 pm
Powered by
PmWiki