Open intsuc opened 2 years ago
Unlike function types with all the parameters erased, the representation of a universal quantification ∀ [] → a : forall [] → α is that of α.
∀ [] → a : forall [] → α
α
Unlike function types with all the parameters erased, the representation of a universal quantification
∀ [] → a : forall [] → αis that ofα.