rodrigogribeiro/agda-software-foundations

Porting of software foundations book to Agda

agda-software-foundations's Issues

Explain about equality proofs and equational proofs

There must be a section explaining about propositional equality and equational reasoning in Agda.

Also, I must include more example of such proofs.

Resolve the pretty printing problems related to LaTeX.

There are many problems related to formatting Agda operators in LaTeX. The problems are mainly related to formatting on lhs2TeX.

Duplicate binding for built-in thing LEVEL

When I'm trying to load Basics.lagda, I get:

/Users/dr/workspace/agda-software-foundations/Basics.lagda:343,1-28

Duplicate binding for built-in thing LEVEL, previous binding to
.Agda.Primitive.Level
when checking the pragma BUILTIN LEVEL Level

Explain inspect idiom

Agda's inspect idiom is the way we simulate a behaviour similar to Coq's remember tactic --- introduce a equality on a expression that we want to pattern match on it, "remembering" its shape before the pattern match.

An explanation of the types used is highly necessary.

Include separeted files to exercices to be solved

In the current version of the "book", exercices are coded in LaTeX code environments. I should put Agda code for exercices in a separated directory for ease working throught the "book" chapters.