LeanInk

LeanInk copied to clipboard

## Description Finally merging the doc-gen LeanInk fork upstream ## Notable Changes Most of the changes are centered around exporting more information in the form of CodeWithInfos so I can...

hargoniX

## Description Attempting to use `leanInk` with a Lean file which relies on `Mathlib`, and following the instructions in the README. My file has the following imports: ``` import Init.Prelude...

femtomc

This doesn't build, but as far as I can tell it's unrelated to the typo fix I made.

hrmacbeth

## Description Copy/paste the output of Alectryon on lean code snippets produces a big mess in your VS code text editor. ## Detailed behaviour Go to [https://leanprover.github.io/lean4/doc/monads/functors.lean.html](https://leanprover.github.io/lean4/doc/monads/functors.lean.html) and select the...

lovettchris

## Current behaviour for code that contains error we get this, and the hover tip correctly shows the error, but there is no visual clue of any error in this...

lovettchris

LeanInk can't install itself for brew-installed elan

10

## Description LeanInk can't install itself for brew-installed elan, the error output is: ``` Installing LeanInk... cp: directory /Users/[MYUSERNAME]/.elan/bin does not exist Failed copying LeanInk to .elan/bin! ``` Under my...

utensil

## Current behaviour The LeanInk code snippets (like those in [functors](http://lovettsoftware.com/lean4/monads/functors.lean.html)) are all nicely annotated by LeanInk, but in the process we lost support for the TryIt button that pops...

lovettchris

Provide the mdbook `# namespace hidden` trick

1

## Description Sometimes while writing you need to quote a piece of core std lib code, but you get errors `already defined` but you also don't want to have readable...

lovettchris

Provide a way to tell leanink to generate comments on #eval, #check commands

2

## Description Readers are saying always visible comments are more readable than the little bubbles we are adding to eval statements. So we should make this an option when generating...

lovettchris

LeanInk silently eats lean compile errors

1

## Description If I have a bug in my book chapter, LeanInk reports these errors in the hover over tooltip, but we need a process to ensure there are no...

lovettchris