Kyle Miller 67bfa19ce0 feat: add quot_precheck for expression tree elaborators (binop%, etc.) (#3078) ... There were no `quot_precheck` instances registered for the expression tree elaborators, which prevented them from being usable in a `notation` expansion without turning off the quotation prechecker. Users can evaluate whether `set_option quotPrecheck false` is still necessary for their `notation` definitions.		2023-12-18 16:52:49 +00:00
..
Precheck.lean	feat: add quot_precheck for expression tree elaborators (binop%, etc.) (#3078)	2023-12-18 16:52:49 +00:00
Util.lean	feat: go to definition for antiquot kinds	2022-08-11 17:46:36 +02:00