[Agda] predicate for sub-type

Andreas Abel andreas.abel at ifi.lmu.de
Sun Feb 3 19:12:56 CET 2013

Hi Serge,

I think that the version that works in your file is the best to define a 
decidable subset of the natural numbers (the one with mem?...\equiv true).

 > And I expected of a simple expression of
 >                                 ... | yes mem=true =  just (n cond' 
 > to work. Because  T (mem? n)  would normalize to  ⊤  on this branch.

A common misunderstanding is that if you do a 'with', then the 
with-expression would reduce to the pattern given in the branch (in your 
case the pattern (yes _)).  But this is not true.
You can get propositional equality if you use the 'inspect pattern' 
(google this, there are messages about this on the agda list).


On 03.02.13 3:01 PM, Serge D. Mechveliani wrote:
> пPeople,
> I have a beginner question about using a predicate to define a subset.
> One variant does type-check, and a `nicer' one does not.
> The program (quite small and simple) and questions are  attached  to this
> letter as
>            Main.agda.zip
> (because I hope that this way I send the math symbols as they are).
> Thanks,
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list