Closed jstolarek closed 3 years ago
I need to test whether quantifiers introduced in a let-signature scope correctly into nested let-signatures:
let x : ∀ a. (a → a) → (a → a) = let y : a → a = λw.w in λz.y in x id_int
where id_int : Int → Int.
id_int : Int → Int
I need to test whether quantifiers introduced in a let-signature scope correctly into nested let-signatures:
where
id_int : Int → Int.