[Agda] rewrite keyword

[Michel Levy]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200330/0da5a1d4/attachment.html>