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

[Martin Escardo]

Thanks. It may be a while until I manage to install this and perform
some sensible tests.

Question: which type theory do you claim to implement with this?

Best,
Martin

On 30/12/15 00:49, Andrés Sicard-Ramírez wrote:
> On 29 December 2015 at 18:46, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>> On 28/12/15 19:09, Nils Anders Danielsson wrote:
>>> I don't know why universe polymorphism and --type-in-type cannot be used
>>> together.
>>
>> I would be lovely if they could be used together.
> 
> I created a branch allowing type in type and universe polymorphism.
> You can get it using
> 
>   $ git clone https://github.com/agda/agda.git
>   $ cd agda
>   $ git checkout issue-1764-maint
>   $ make install-bin
> 
> Enjoy,
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe