search

ualib / agda-algebras

The Agda Universal Algebra Library (html docs available at the url below)
https://ualib.github.io/agda-algebras/
Creative Commons Attribution Share Alike 4.0 International
29 stars 7 forks source link

clean up and clarify informal and formal proofs of hsp in Sec 6 #194

Closed williamdemeo closed 2 years ago

williamdemeo commented 2 years ago

Hopefully this makes it easier to address some of the issues raised about the formal and informal proofs of hsp in Sec 6

williamdemeo commented 2 years ago

oops, I meant Sec 6 in my commit message

williamdemeo commented 2 years ago

That does add more guiding English to a part of the paper that was indeed especially terse. Hopefully it won't cause space issues?

Great, thanks. I think it's still just under 20 pages not including the some of the references.

JacquesCarette commented 2 years ago

Can you quickly remind me how to 'make' the paper?

williamdemeo commented 2 years ago

Oh, sorry, it's in the README.md file in the TYPES2021 directory, which says the following:

Here is the workflow used to develop the document agda-hsp.pdf.

  1. Edit/improve the literate Agda file src/Demos/HSP.lagda.
  2. Invoke agda --latex --latex-dir=doc/TYPES2021 src/Demos/HSP.lagda from the main agda-algebras directory.
  3. Invoke pdflatex agda-hsp from within the doc/TYPES2021 directory.

On Mon, Apr 25, 2022 at 5:48 PM Jacques Carette @.***> wrote:

Can you quickly remind me how to 'make' the paper?

— Reply to this email directly, view it on GitHub https://github.com/ualib/agda-algebras/pull/194#issuecomment-1109073966, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA25MJAA7JHDAYQVUSHQKCLVG4HJHANCNFSM5UJI46CA . You are receiving this because you modified the open/close state.Message ID: @.***>