[Agda] More rewrite woes
fdhzs2010 at hotmail.com
Sun Jan 9 17:38:54 CET 2022
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.
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 18.104.22.168-fce01db.
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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda