[Agda] Undocumented (Recursive?) Positivity Checking

[Yotam Dvir]

Thanks! Where can I find more information about these command-line options that don’t appear in the documentation (like -vtc)?

> On 15 Oct 2019, at 16:36, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> 
> On 15/10/2019 14.11, Nils Anders Danielsson wrote:
>> $ agda -vtc.polarity:10 Test.agda
>> Checking Test ([…]/Test.agda).
>> Polarity of Test.List: [*, +]
>> Polarity of Test.List.[]: [*, *]
>> Polarity of Test.List._∷_: [*, *]
>> Polarity of Test._∷_-0: [*, *, *]
>> Polarity of Test._∷_-1: [*, *, *]
> 
> This answer may have been somewhat misleading. As far as I recall the
> polarities are not used by the positivity checker. I think the following
> information might be more relevant to your question:
> 
> $ agda -vtc.pos:10 --ignore-interfaces Test.agda | grep "args of List"
> checking args of List
> args of List = [-[_]->, -[g+]->]
> 
> -- 
> /NAD