thorimur
thorimur
!bench
I'm new to using mermaid, but would find this very useful for my application. However, from the perspective of a new user, I'd like to mention that trying to remember...
Yes, I believe this one's for real. :) It introduces the possibility of `isDefEq` failing where it otherwise wouldn't. Contrast with #3473 (an alternate more experimental approach to the same...
WIP
Makes sense! (I wish VS code would let us access the result of parsing somehow...) Just to be clear, do you consider adding some indentation but not enough indentation to...
@semorrison Apologies, I've been inactive for the past few months! :) If this is still desired I'm happy to finalize it and make it a real PR.
Here's a [link](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Meta.2EsynthInstance.2Eanswer.20not.20registered/near/421955563) to the message, and here are the ones I identified: ``` Lean/PrettyPrinter/Delaborator/Basic.lean: PrettyPrinter.delab.input Lean/Meta/Tactic/Simp/SimpAll.lean: Meta.Tactic.simp.all Lean/Meta/DecLevel.lean: Meta.isLevelDefEq.step Lean/Meta/SizeOf.lean: Meta.sizeOf.minor Lean/Meta/SizeOf.lean: Meta.sizeOf.minor.step Lean/Meta/SizeOf.lean: Meta.sizeOf.aux Lean/Meta/SizeOf.lean: Meta.sizeOf.loop Lean/Elab/StructInst.lean: Elab.struct.modifyOp...
Hmm, I'm not *totally* sure about only linting the silent commands, because it's nice to have an error telling you explicitly what's wrong! But I do like having it show...