Search results

Missing Licence

Status: Open.

#16 In leanprover/lean3-web-editor;

· Mohammad-Amjed opened on Jul 4, 2023

Bad \/ substitution in online editor leaves behind syntax-error-causing hidden zero-width characters

Status: Open.

#8 In leanprover/lean3-web-editor;

· Strilanc opened on Aug 22, 2022

Pretty substitution of backslashed keywords doesn't occur unless a space terminates the keyword

Status: Open.

#5 In leanprover/lean3-web-editor;

· leodemoura opened on Mar 1, 2018

fetch_lean_js.sh script is platform specific

Status: Open.

#4 In leanprover/lean3-web-editor;

· Antony74 opened on Feb 27, 2018

Brackets not escaped in Live urls - can't post them to StackOverflow

Status: Open.

#2 In leanprover/lean3-web-editor;

· Antony74 opened on Feb 14, 2018

Space-triggered '\<symbol>' autocompletion messes up cursor position

Status: Open.

#1 In leanprover/lean3-web-editor;

· khoek opened on Nov 14, 2017