lean4-metaprogramming-book icon indicating copy to clipboard operation
lean4-metaprogramming-book copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

metam: add note about matching expressions with `isDefEq`

Open JLimperg opened this issue 3 years ago • 0 comments
trafficstars

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.

JLimperg avatar Jul 26 '22 10:07 JLimperg