GitHub · Where software is built

This repository was archived by the owner on Aug 24, 2024. It is now read-only.

Labels Milestones

Error when analyzing a simple file with <code>LeankInk</code>: <code>failed to read file ..., invalid header</code>

#59

· mariovagomarzal opened

on Aug 13, 2024

Using <code>Mathlib</code> as an import causes <code>leanInk</code> to error

#56

· femtomc opened

on Dec 28, 2023

We need to get back the "Copy to clipboard" button on Lean code snippets

#35

· lovettchris opened

on Oct 8, 2022

Red squiggles

#34

· lovettchris opened

on Sep 8, 2022

We need to get back the "Try It" button when manual is read inside VS code documentation view

#32

· lovettchris opened

on Sep 2, 2022

Provide the mdbook <code># namespace hidden</code> trick

#30

· lovettchris opened

on Aug 31, 2022

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

#29

· lovettchris opened

on Aug 30, 2022

Hiding certain Lean imports at the beginging of a chapter

#25

· lovettchris opened

on Aug 26, 2022

LeanInk silently eats lean compile errors

#24

· lovettchris opened

on Aug 26, 2022

LeanInk has trouble with infix operators

#23

· lovettchris opened

on Aug 25, 2022

Colorization difference

#22

· lovettchris opened

on Aug 25, 2022

LeanInk can't install itself for brew-installed elan

#21

· utensil opened

on Aug 1, 2022