feat: partial_fixpoint #253
Conversation
Manual/Meta/Monotonicity.lean
Outdated
| let targetStx : TSyntax `term ← | ||
| forallTelescope ci.type fun _ concl => do | ||
| unless concl.isAppOfArity ``Lean.Order.monotone 5 do | ||
| throwError "Unexpecte conclusion of {name}" | ||
| let f := concl.appArg! | ||
| unless f.isLambda do | ||
| throwError "Unexpecte conclusion of {name}" | ||
| lambdaBoundedTelescope f 1 fun _ _call => do | ||
| -- Could not get this to work: | ||
| -- let _stx ← Lean.PrettyPrinter.delab call | ||
| -- `(Inline.code $(quote stx)) | ||
| `(Inline.text "TODO") | ||
| -- pure (some stx) |
There was a problem hiding this comment.
I dug my toes into the Manual.Meta realm, because I’d like to auto-generate a list of registered monotonicity lemmas. This worked fine, and I found how to pretty print the name of the lemma. But I’d also include some expressions that I want to calculate from the type. The above didn’t work, probably because of one level of quotation too little.
I guess I could pretty-print to a string and include that…
But can I also “delaborate” an Expr to something that I can put in Inline.code so that it’s highlighted and hovers work?
There was a problem hiding this comment.
I also tried to use a table instead of a ul, but my attempt at 56b0219 also ran into my ignorance of how verso works. Maybe we can have a quick look together next week, during tea time or else.
|
Ok, marking this as ready for review for now, and will try to keep my hands away from it. I’ll merge the feature to Lean4 I left some |
|
Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 8478f38. |
The manual section to go with leanprover/lean4#6355.