Tan Yee Jian

Fix typos and exercise file in part 1 of book

1

Not sure if there is a better way to edit the code for `twice`, where an implementation is given and readers are expected to fill in a missing type declaration.

Download not working. Hogs up CPU usage with beam.smp

3

 when running `mix fluminus --download-to=/path/to/my/dir`. Works fine previously until recently. OS: Ubuntu 19.10 Tell me if more info is needed!

The current link in the header, "Index", points to a non-existent page `indexpage.html` (https://metacoq.github.io/html/indexpage.html), while the index is actually generated in `index.html` (https://metacoq.github.io/html/index.html). There are two ways to fix this:...

Implement a --cubical-without-glue option

7

This pull request aims to implement a `--cubical-without-glue` pragma option that allows one to use Cubical features, but disallowing the primitive Glue type. This is in anticipation of my ongoing...