[Agda] rewrite keyword

[a.j.rouvoet]

Hi Michel,

Re 1) in general many inputs are behind menus. If you input \^l you 
should get a menu at the bottom that you can choose other options from.
If you copy paste a symbol into emacs, select it and call describe-char, 
it should also tell you how to input it using agda-input.

Others can probably answer your question about rewrite better than I can :)

Cheers,


Arjen

On 3/30/20 9:49 PM, Michel Levy wrote:
>
> In an exercise of https://plfa.github.io/Relations/ You have the 
> following definition
>
> +-monoˡ-≤ <https://plfa.github.io/Relations/#17419> : ∀ (m 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17434> n 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17436> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17438> : ℕ 
> <https://plfa.github.io/Relations/Agda.Builtin.Nat.html#165>) → m 
> <https://plfa.github.io/Relations/#17434> ≤ 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#1195> n 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17436> → m 
> <https://plfa.github.io/Relations/#17434> + 
> <https://plfa.github.io/Relations/Agda.Builtin.Nat.html#298> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17438> ≤ 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#1195> n 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17436> + 
> <https://plfa.github.io/Relations/Agda.Builtin.Nat.html#298> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17438>
>
> +-monoˡ-≤ <https://plfa.github.io/Relations/#17419> m 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17501> n 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17503> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17505> m≤n 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17507> 
> rewrite +-comm 
> <https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911> 
> m <https://plfa.github.io/Relations/plfa.part1.Relations.html#17501> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17505> | 
> +-comm 
> <https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911> 
> n <https://plfa.github.io/Relations/plfa.part1.Relations.html#17503> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17505> = 
> +-monoʳ-≤ 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#16619> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17505> m 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17501> n 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17503> m≤n 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17507>
>
> On this example, I have two questions
>
>
> 1) How to have the superscript l in the name +-monol
>
> On my emacs \^l give a right to left superscript arrow
>
>
> 2) Why
>
> +-monoˡ-≤ <https://plfa.github.io/Relations/#17419> m 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17501> n 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17503> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17505> m≤n 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17507> 
> rewrite +-comm 
> <https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911> 
> m <https://plfa.github.io/Relations/plfa.part1.Relations.html#17501> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17505> | 
> +-comm 
> <https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911> 
> n <https://plfa.github.io/Relations/plfa.part1.Relations.html#17503> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17505>
>
> is not a term ?
>
> To understand the meaning of rewrite, I try to get the type of
>
> \lambda m n p m <https://plfa.github.io/Relations/#17419>≤ 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17507>n -> 
> ag+-monoˡ-≤ <https://plfa.github.io/Relations/#17419> m 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17501> n 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17503> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17505> m≤n 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17507> 
> rewrite +-comm 
> <https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911> 
> m <https://plfa.github.io/Relations/plfa.part1.Relations.html#17501> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17505> | 
> +-comm 
> <https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911> 
> n <https://plfa.github.io/Relations/plfa.part1.Relations.html#17503> p 
> <https://plfa.github.io/Relations/plfa.part1.Relations.html#17505>
>
> But this is not a term, and I got a parse error.
>
> More generally, why isn't there a term of the form (exp1 rewrite exp2)  ?
>
> PS : I have read the doc 
> "https://agda.readthedocs.io/en/latest/language/with-abstraction.html#with-rewrite"
>
> -- 
> courriel : michel.levy.imag at free.fr
> mobile : 06 59 13 42 53
> web : michel.levy.imag.free.fr
>
> _______________________________________________
> 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/20200330/8a9954c4/attachment.html>