Printing fine-grained delaboration structure #23

New Issue

aniva · 2023-10-26T22:52:48-07:00

aniva commented

2023-10-26 22:52:48 -07:00

In Lean's source code there's this file src/lean/Lean/PrettyPrinter/Delaborator/Basic.lean. Maybe this can be used to print a delaborated sexp so we don't have to do sketchy alignment heuristics

In Lean's source code there's this file `src/lean/Lean/PrettyPrinter/Delaborator/Basic.lean`. Maybe this can be used to print a delaborated sexp so we don't have to do sketchy alignment heuristics

aniva added this to the 0.3 milestone 2023-10-26 22:52:48 -07:00

aniva added the

category

feature

label 2023-10-26 22:52:48 -07:00

aniva added the

priority

low

label 2023-11-30 01:04:45 -08:00

aniva removed this from the 0.3 milestone 2024-03-18 10:11:45 -07:00

aniva changed title from ~~Print a delaborated sexp~~ to Printing fine-grained delaboration structure

2024-04-11 17:56:13 -07:00

aniva commented

2024-09-08 01:10:47 -07:00

Alignment heuristics are not needed in Trillium anymore. This could still be useful to just provide training data, but I don't see a way to inject code into the Delab monad.

Alignment heuristics are not needed in Trillium anymore. This could still be useful to just provide training data, but I don't see a way to inject code into the `Delab` monad.

Sign in to join this conversation.