agda2hs icon indicating copy to clipboard operation
agda2hs copied to clipboard

Published 20 hours ago • verified publisher icon agda

Rewrite construct

Open flupe opened this issue 1 year ago • 1 comments

Not being able to use the rewrite construct is proving to be extremely annoying.

Related: #40, #255.

flupe avatar Dec 21 '23 11:12 flupe

I find that using the cong! tactic together with equational reasoning is a useful substitute for the rewrite construct.

HeinrichApfelmus avatar Jan 26 '24 13:01 HeinrichApfelmus