[Agda] More rewrite woes

Jason Hu fdhzs2010 at hotmail.com
Sun Jan 9 17:38:54 CET 2022

Hi Phil,

Your rewrite is an no-op, because the goal does not have the corresponding left hand side:

Goal: reflᴳ ⊢ M ↑ p ≤ᴹ M ↑ p ⦂ id
Have: (id ⨟ p) ≡ p

You can apply reflexivity to rewrite all p to (id ⨟ p) but this is not want you want. In Agda you cannot specify which p to rewrite so I suppose this is a limitation. There is nothing wrong with the current solution you have.

Jason Hu

From: Philip Wadler<mailto:wadler at inf.ed.ac.uk>
Sent: Sunday, January 9, 2022 10:56 AM
To: Agda mailing list<mailto:agda at lists.chalmers.se>
Subject: [Agda] More rewrite woes

I've attached code where a rewrite should work but does not. There are many places in the full development where I encounter similar issues. Rewrite works fine in the original definition of left-id, but not in the subsequent attempt to prove reflᴹ. Any advice on how to fix it?

The file is cut down from the original---I apologise that it is still rather lengthy. The issue with rewrite appears at the end. I am using Agda version

Thank you for your help! Go well, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220109/cd16cddf/attachment-0001.html>

More information about the Agda mailing list