[Agda] Is it possible to switch off universes checking?

[Andreas Abel]

effectfully, Martin,

I pushed a commit to make --type-in-type work with universe 
polymorphism.  Please check if it suits your needs (and report bugs, if 
any).

Cheers,
Andreas

On 31.12.2015 05:18, effectfully wrote:
> Nils Anders Danielsson, thanks, it worked.
>
> Ulf Norell, your code typechecks. Moreover both
>
>      ok : Set
>      ok = id Set
>
> and
>
>      ok : Set₁
>      ok = id Set
>
> typecheck without unresolved metas.
>
> This
>
>      data D α β : Set β where
>        C : Set α -> D α β
>
> is OK too.
>
> However
>
>      data D {α} (A : Set α) : Set where
>        C : A -> D A
>
> results in
>
>      Set != Set α
>      when checking the constructor C in the declaration of D
>
> Andrés Sicard-Ramírez, thanks for your effort.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/