Using "Refl" as the solution for test_factorial1 (or 2) yields:

 |   When checking right hand side of testFactorial1 with expected type
 |           factorial 3 = 6
 |   
 |   Type mismatch between
 |           6 = 6 (Type of Refl)
 |   and
 |           factorial 3 = 6 (Expected type)
 |   
 |   Specifically:
 |           Type mismatch between
 |                   6
 |           and
 |                   factorial 3

This is important because (1) no other tactics have been introduced at this point and (2) later in the chapter, we explicitly claim that it is solvable that way:

Now that we've defined a few datatypes and functions, let's turn to stating and
proving properties of their behavior. Actually, we've already started doing
this: each of the functions beginning with \idr{test} in the previous sections
makes a precise claim about the behavior of some function on some particular
inputs. The proofs of these claims were always the same: use \idr{Refl} to check
that both sides contain identical values.

For now, it's copied rather directly from the Coq.

@jfdm (or anyone else with sufficient permissions), could you please grant commit rights to @clayrat? At this point he's contributing more than I am, and I think it'd be nice if he and I (at least) could trade off reviews and merging.

It would also be good to set the default branch to develop (and/or grant me access to the repo settings). Related: #15

Cheers!

• Use 1.1.0 (related: #20)
• Ensure we can at least build this iPKG

Related: NixOS/nixpkgs#26014

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

e.g. https://github.com/david-christiansen/idris-code-highlighter/blob/master/CONTRIBUTING.md

A link to pdf in README returns 404.

Figure out why 944bc3c breaks the PDF build.

As discussed in #17, Pruviloj, as currently used in the Tactics chapter is probably too experimental to be introduced so early in the book.

My proposal is to re-do the first half with dependent pattern matching (possibly discussing its use vs rewrites), rename the chapter to smth like PatternMatching and keep the original half as an appendix named Tactics or even Pruviloj.

• Do we want these?
• Should we host them on the site too?
• This will require updating pandoc-minted.hs to support HTML
• link them on the site

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

Related: #25

Poly.lidr note of:
https://github.com/idris-hackers/software-foundations/blob/develop/src/Poly.lidr#L1027

Can be solved written as:

succ' : (n : Nat' {x}) -> Nat' {x}
succ' n = \f, x => f (n f x)

succ'_1 : succ' Church.zero f x = one f x
succ'_1 = Refl

succ'_2 : succ' Church.one f x = two f x
succ'_2 = Refl

succ'_3 : succ' Church.two f x = three f x
succ'_3 = Refl

Omitting f, x, or Church will cause issues.
Having to provide f and x seems necessary to collapse the lambdas, if that wording makes sense at all.
Having to provide Church is part of a problem Idris seems to have in deciding whether something lowercase is an identifier from elsewhere or a fresh type variable.

This isn't a PR since I'm not 100% on what is considered good style yet but I wanted to share that there is a solution.

• ineline
• mintline
• ...

Some special characters are duplicated in the output. In particular,

• %
• #

Both are special in LaTeX, which is why I suspect this is happening.

TODO

• Describe my general plan
  • Copy text
  • Translate code idiomatically
  • Update (edit/augment/delete) text accordingly
  • ... ?
• Firm up prerequisites (related: #10)
• Maybe get a good shell.nix sorted (TeX in Nix is pretty broken atm...)
• Solicit contributions
• Describe the pandoc workflow, including the hybrid GFM/TeX Literate Idris.
• Consider ditching the hybrid GFM madness for regular LaTeX
  This turned out to be more annoying that it seemed worth, so I abandoned the idea.

Ideally we can resolve or remove all the \todos, edit the text, format the code (see #39, #24 [\subsection hack works], #22, #35 [adopt Iosevka] and maybe #25/#30, et al.)

https://softwarefoundations.cis.upenn.edu/draft/

Small question. In the Basics in More Exercises we have task negation_fn_applied_twice. I'm not sure we have a way to solve it using just rewrite (it looks like task is to solve it by rewrite). I was not able to solve it by using rewrite (replace has helped). I'm not sure if it its just me or the task requires a bit more knowledge.

• Introduction
• Enumerated Types
  • Edit first two paragraphs
  • Days of the Week
    • Verify that top-level type signatures are optional required and edit paragraph accordingly
    • Discuss interactive editor support
    • Reword "... after some simplification"
    • Verify the "main uses" claim
  • Booleans
    • Edit the syntax paragraph
  • Function types
    • Confirm the "function types" wording
  • Modules
    • Flesh out description of Idris's module system
    • Discuss namespaces
  • Numbers
    • Figure out how to redefine Nat locally, as in the Coq inner modules, Playground1 and Playground2.
      • plus
      • mult
      • minus
    • Verify the commentary on "wildcard pattern"
• Proof by Simplification
• Proof by Rewriting
• Proof by Case Analysis
  • More on Notation (Optional)
  • Fixpoint and Structural Recursion (Optional)
• More Exercises

For example, <-> looks bad in Monoid and it doesn't render ∀, et al.

Idris version 1.3.2

mult : (n, m : Nat) -> Nat
mult Z = Z
mult (S k) = plus m (mult k m)

Should be

mult : (n, m : Nat) -> Nat
mult Z _ = Z
mult (S k) m = plus m (mult k m)

The license has been updated upstream, and is a lot clearer now.

https://softwarefoundations.cis.upenn.edu/lf-current/

See #32

For example: 5b014ec removes some innocent-looking...

\todo[inline]{...}

... calls that broke the PDF build on my system.

• CTAN: Package todonotes

• Document the workaround

Should the text be kept in perfect sync with the original? The book keeps getting minor updates to phrasing, e.g.:

• https://github.com/idris-hackers/software-foundations/blob/master/src/Preface.lidr#L22 - the book now says "offshoot" chapters instead of "appendices"
• https://github.com/idris-hackers/software-foundations/blob/master/src/Preface.lidr#L52 - the book removed the idea of part

etc..