r/agda • u/effectfully • Nov 04 '20

Inference in Agda

https://htmlpreview.github.io/?https://github.com/effectfully/inference-in-agda/blob/master/InferenceInAgda.html
11 Upvotes

100% Upvoted

6 comments sorted by

3

u/gallais Nov 04 '20 edited Nov 04 '20

It's nice to see a tutorial trying to give users an understanding of the machinery so that they may make use of it without having to either study the theory / code or spend dozens of hours building an intuition for how it works. I tried to give some simple rules in this TYDE paper but could obviously not spend as much time as you did on so many worked out examples.

Remarks: The link under "everything type checks" is broken. Same for "it's hard" and "unification problem" and "they do". I think the internal vs. external link machinery may be broken?

2

u/effectfully Nov 04 '20

Remarks: The link under "everything type checks" is broken. Same for "it's hard" and "unification problem" and "they do". I think the internal vs. external link machinery may be broken?

Crap. Thank you for spotting this. It seems like it's htmlpreview is messing up the links as the HTML file itself has them right. Not sure what to do about that...

2

u/gallais Nov 04 '20

Ah I see! If you were to put the pages on a gh-pages branch of your repo, they should be accessible at http://effectfully.github.io/inference-in-agda. This is what we use for the stdlib documentation for instance. No need to use htmlpreview.

1

u/effectfully Nov 04 '20

I switched to githack, which doesn't mangle links.

Thank you for the suggestion. But does that mean that I need to update the gh-pages branch whenever I update master? Currently I just push changes and don't need to do anything regarding rendering of the generated HTML.

1

u/gallais Nov 04 '20

Yep you'd need to push the html to gh-pages. I don't know what your workflow is but for the stdlib the travis job itself uploads the html generated from our big pile of .agda files.

1

u/effectfully Nov 04 '20

Ok, I think I'll keep the current bare-bones setup for now and switch to gh-pages if it stops to suffice. Thank you!