[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'
⊤.tt)
> 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'

Cheers,
Andreas

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
http://www2.tcs.ifi.lmu.de/~abel/
`