Eric Bailey

Consider adopting LSP for editor support

2

This might be better suited for [alpaca-mode](https://github.com/alpaca-lang/alpaca-mode) et al., but [LSP](https://github.com/Microsoft/language-server-protocol) looks like a cool standard to adopt for editor support.

Support types with same name and different arities

2

As a user, I'd like to define a type `foo/1` as well as a type `foo/2`: ```ocaml type foo 'a = Nothing | Just 'a type foo 'a 'b =...

WIP: Edit Preface

3

This is intended to resolve #2. ----- ```fish ag todo src/Preface.lidr ``` TODO: update todo list

https://github.com/david-christiansen/idris-code-highlighter Related: #25

Finish Basics

1

- [x] Introduction - [ ] Enumerated Types - [ ] Edit first two paragraphs - [ ] Days of the Week - [x] Verify that top-level type signatures are...

Write more idiomatic Idris

3

While this is a translation of a book written for/in Coq, we should use idiomatic Idris whenever possible.

Generate HTML files

3

- Do we want these? - Should we host them on the site too? - This will require updating [`pandoc-minted.hs`](https://github.com/idris-hackers/software-foundations/blob/develop/src/pandoc-minted.hs) to support HTML - [ ] link them on the...

Resolve todonotes issues

1

For example: 5b014ec246f752df4a5297b4609ae9bfa6ab8f70 removes some innocent-looking... ```latex \todo[inline]{...} ``` ... calls that broke the PDF build on my system. - [CTAN: Package todonotes](https://ctan.org/pkg/todonotes) - [ ] Document the workaround

Figure out why 944bc3ca4dee87120682cbce20134caa0b15808a breaks the PDF build.