Questions tagged [scopedenvextension]
The scopedenvextension tag has no usage guidance.
1
question
1
vote
0
answers
20
views
How to debug a Lean4 extension
I am interested in debugging the NormCastExt extension to better understand how it works (https://github.com/leanprover/std4/blob/5aa4ab4f0c096e8d0600e3ae41b8577dcf6edb13/Std/Tactic/NormCast/Ext.lean#...
- 217