[Agda] congruence, Preserves_2

[Andreas Abel]

On 08.09.12 8:43 PM, Serge D. Mechveliani wrote:
> On Sat, Sep 08, 2012 at 10:38:26PM +0400, Serge D. Mechveliani wrote:
> [..]
>>    p : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
>>    p m n p =  ?
> [..]

Yeah, I was surprised to see that is legal to shadow the function p 
being defined by one of its parameters p, but apparently it is (also in 
Haskell).

>
> For any occasion, change it to
>
>    proo : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
>    proo m n p =  ?


-- 
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/