ee8acc14e2
This PR fixes a `grind` internal error triggered when `cast` (or `Eq.rec`, `Eq.ndrec`, `Eq.recOn`) is applied to an argument that has not yet been internalized. `pushCastHEqs` was emitting `e ≍ a` before internalizing the args of `e`, so the `rhs` of the heq had no enode and the debug sanity check tripped. The call now runs after the args are internalized.
7 lines
267 B
Text
7 lines
267 B
Text
module
|
||
|
||
set_option grind.debug true in
|
||
theorem test {β α} {γ : β → Sort v} {f : α → β} {g : β → α}
|
||
(h : Function.LeftInverse g f) (C : ∀ a : α, γ (f a)) (a : α) :
|
||
cast (congrArg (fun a ↦ γ (f a)) (h a)) (C (g (f a))) = C a := by
|
||
grind
|