[Agda] Re: elements of recursive records

[Thorsten Altenkirch]

Oops this is so easy that I feel stupid for asking.

I guess i forgot the golden rule of working with ∞  : don't use ♯ locally.

Or do you have a better way to put it.

Thanks a lot,
Thorsten


On 28 Mar 2011, at 17:29, Nils Anders Danielsson wrote:

> On 2011-03-28 16:59, Thorsten Altenkirch wrote:
>> but Agda doesn't like this - i suspect it has to do with # appearing
>> in a type. But I don't see how to avoid this - do you?
> 
> reflω′ : ∀ {A} (a : A) → ∞ (El (♭ (hom (Idω A) a a)))
> reflω′ a = ♯ record { obj→ = refl; hom→ = reflω′ refl }
> 
> reflω : ∀ {A} (a : A) → El (♭ (hom (Idω A) a a))
> reflω a = ♭ (reflω′ a)
> 
> -- 
> /NAD
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda