[Agda] Recursive Sets / refine vs. load

Nils Anders Danielsson nad at chalmers.se
Sat Mar 24 23:13:10 CET 2012

On 2012-03-24 18:12, Brandon Moore wrote:
> The following definition looks reasonable to me,
> the type of the hole is reported as ℕ → Set,
> and refine/give accepts what I've written there,
> but then typechecking the file fails, saying
> t true !=< ℕ of type Set


> t : Bool → Set
> t true = ℕ
> t false = Σ (t true) {!Vec Bool!}
> Why isn't this definition accepted?

Because (non-mutual) definitions are not unfolded before they have been
type-checked. Unfortunately this does not apply to goals: Agda forgets
that t should not unfold when Vec Bool is type-checked. This is a
long-standing bug:



More information about the Agda mailing list