[Agda] Recursive Sets / refine vs. load

Peter Hancock hancock at spamcop.net
Sat Mar 24 21:19:32 CET 2012

On 24/03/2012 17: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
> module test where
> open import Data.Nat
> open import Data.Bool
> open import Data.Product
> open import Data.Vec
> t : Bool → Set
> t true = ℕ
> t false = Σ (t true) {!Vec Bool!}
> Why isn't this definition accepted?

I'd like to hear the real explanation, but I imagine that
when Mrs Agda is type checking the second equation, she isn't
paying much attention to the first equation, beyond thinking that
it type checks.  Anymore than if you had written

> t false = Σ (t true) {!Vec Bool!}
> t true = ℕ

I'm not sure she should be blamed.  Is there a general scheme
(like natrec, or elim\exists, or something) she should be taught?
(I'm not trying to be funny. I agree it's sad when you can "give"
something but she won't ^C^L it.  I think it's inevitable.)


More information about the Agda mailing list