[Agda] type:type locally?

[Jesper Cockx]

Thanks to the great power of procrastination, I present to you: the {-#
NO_UNIVERSE_CHECK #-} pragma!

https://github.com/agda/agda/commit/be89d4a8b264dd2719cb8c601a2c7f45a95ba220

Enjoy and let me know if there's any problems with it. Now let's get back
to writing ;)

-- Jesper

On Wed, Jun 27, 2018 at 2:40 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> Hi Thorsten,
>
> Currently we do not have such an option. I think it would make sense to
> add a pragma for disabling the universe check for a data/record type
> without disabling universe checking entirely. This would actually be easier
> to implement than NO_POSITIVITY_CHECK, as the universe check is done for a
> single data/record type rather than the whole mutual block. If there are no
> takers I could take a look at it (probably only after the POPL deadline
> though).
>
> -- Jesper
>
> On Tue, Jun 26, 2018 at 11:52 AM, Thorsten Altenkirch <
> Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>
>> I can switch off positivity checking locally by saying
>>
>>
>>
>> {-# NO_POSITIVITY_CHECK #-}
>>
>>
>>
>> But I can’t say
>>
>>
>>
>> {-# TYPE-IN-TYPE #-}
>>
>> data Prop : Set
>>
>> T : Prop → Set
>>
>>
>>
>> data Prop where
>>
>>   pi : (A : Set)(b : A → Prop) → Prop
>>
>>
>>
>> T (pi A b) = (x : A) → T (b x)
>>
>>
>>
>> Or is there a difference syntax? This would be useful for a simple-minded
>> encoding of the calculus of constructions.
>>
>>
>>
>> Thorsten
>>
>>
>>
>> P.S. I know I can avoid this by adding another level:
>>
>>
>>
>> data Prop : Set
>>
>> T : Prop → Set
>>
>> data U : Set
>>
>> El : U → Set
>>
>>
>>
>> {-# NO_POSITIVITY_CHECK #-}
>>
>> data U where
>>
>>   prop : U
>>
>>   pi : (a : U)(b : El a → U) → U
>>
>>   emb : Prop → U
>>
>>
>>
>> El prop = Prop
>>
>> El (pi a b) = (x : El a) → El (b x)
>>
>> El (emb p) = T p
>>
>>
>>
>> data Prop where
>>
>>   pi : (a : U)(b : El a → Prop) → Prop
>>
>>
>>
>> T (pi a b) = (x : El a) → T (b x)
>>
>> This message and any attachment are intended solely for the addressee
>> and may contain confidential information. If you have received this
>> message in error, please contact the sender and delete the email and
>> attachment.
>>
>> Any views or opinions expressed by the author of this email do not
>> necessarily reflect the views of the University of Nottingham. Email
>> communications with the University of Nottingham may be monitored
>> where permitted by law.
>>
>>
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180629/a620f327/attachment.html>