[Agda] how to run this rewrite example

[Martin Stone Davis]

Just to get the example running, you could make it a postulate. Then you
don't have to bother providing a proof.

postulate
  plus-commute : (a b : Nat) → a + b ≡ b + a



--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com

On Fri, Feb 5, 2016 at 8:05 PM, Mandy Martino <tesleft at hotmail.com> wrote:

> Hi ,
>
>
> when run the code directly, it return missing definition,
>
> how to write this definition?
>
>
> bb.agda:26,1-13
>
> Missing definition for plus-commute
>
> Following
>
>
> http://agda.readthedocs.org/en/latest/language/with-abstraction.html#rewrite
> With-Abstraction — Agda 2.5 documentation
> <http://agda.readthedocs.org/en/latest/language/with-abstraction.html#rewrite>
> agda.readthedocs.org
> The clause containing the with-abstraction has no right-hand side. Instead
> it is followed by a number of clauses with an extra argument on the left,
> separated from ...
>
> open import Prelude
>
> data Bool2 : Set where
>  true : Bool2
>  false : Bool2
>
> not2 : Bool2 -> Bool2
> not2 true = false
> not2 false = true
>
> identity2 : (A : Set) -> A -> A
> identity2 A x = x
>
> data Nat2 : Set where
>  zero2 : Nat2
>  suc : Nat2 -> Nat2
>
> _or2_ : Bool2 -> Bool2 -> Bool2
> false or2 x = x
> true or2 _ = true
>
> if2_then2_else2_ : (A : Set) -> Bool2 -> A -> A -> A
> if2 true then2 x else2 y = x
> if2 false then2 x else2 y = y
>
> plus-commute : (a b : Nat) → a + b ≡ b + a
>
> thm : (a b : Nat) → P (a + b) → P (b + a)
> thm a b t with   a + b  | plus-commute a b
> thm a b t    | .(b + a) | refl = t
>
> main =
>  if2_then2_else2_ Bool2 true (putStrLn "it is true") (putStrLn "it is else
> case")
>  putStrLn "Hello World"
>
>
> Regards,
>
> Martin
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160206/13921024/attachment.html