[Agda] predicate for sub-type

[Andreas Abel]

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' 
(google this, there are messages about this on the agda list).

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/