The MetaM chapter already contains some notes about matching expressions up to computation, using whnf. But arguably the more convenient approach is to use isDefEq with a pattern expression containing some metavariables (like the quote4 library). I should add a note about this trick.
The MetaM chapter already contains some notes about matching expressions up to computation, using
whnf
. But arguably the more convenient approach is to useisDefEq
with a pattern expression containing some metavariables (like thequote4
library). I should add a note about this trick.