iris-lean icon indicating copy to clipboard operation
iris-lean copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Evaluate possibilities for expression quotation

Open larsk21 opened this issue 2 years ago • 0 comments

The tactic implementations need to destruct expressions (Expr), which is currently done by hand, i.e. using methods like isAppOf and getAppArgs in Iris/Std/Expr.lean. Using expression quotations would presumably simplify this process. One package to check out is quote4.

larsk21 avatar Oct 26 '22 15:10 larsk21