I have a situation where a rewrite unexpectedly does nothing. How is this possible? I would expect a failed rewrite to give an error message, otherwise I expect the goal type to change.
I have minimised the proof script to the following:
module Gamma where
open import Relation.Binary.PropositionalEquality
record Semiring : Set₁ where
field
grade : Set
1R : grade
_*_ : grade → grade → grade
leftUnit* : {r : grade} → 1R * r ≡ r
-- [...]
open Semiring {{...}}
foo : {{R : Semiring}} {r : grade} → 1R * r ≡ r
foo {r = r} rewrite leftUnit* {r} = {! !}
Without the rewrite, the goal is (R Semiring.* Semiring.1R R) r ≡ r. Adding the rewrite neither changes the goal, nor gives any error message.
Note: This is easy enough to work around, but I wanted to understand what is going on here.
Addendum$ agda --version
Agda version 2.6.4.1
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4