idris-hackers / software-foundations Goto Github PK
View Code? Open in Web Editor NEWSoftware Foundations in Idris
Home Page: https://idris-hackers.github.io/software-foundations
License: MIT License
Software Foundations in Idris
Home Page: https://idris-hackers.github.io/software-foundations
License: MIT License
Should the text be kept in perfect sync with the original? The book keeps getting minor updates to phrasing, e.g.:
"offshoot" chapters
instead of "appendices"
the idea of
partetc..
pandoc-minted.hs
to support HTMLUsing "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 example, <->
looks bad in Monoid and it doesn't render โ, et al.
Some special characters are duplicated in the output. In particular,
%
#
Both are special in LaTeX, which is why I suspect this is happening.
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.
See #32
The license has been updated upstream, and is a lot clearer now.
A link to pdf in README returns 404.
For now, it's copied rather directly from the Coq.
Related: NixOS/nixpkgs#26014
syntax
paragraphNat
locally, as in the Coq inner modules, Playground1
and Playground2
.plus
mult
minus
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.
@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!
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 rewrite
s), rename the chapter to smth like PatternMatching
and keep the original half as an appendix named Tactics
or even Pruviloj
.
shell.nix
sorted (TeX in Nix is pretty broken atm...)pandoc
workflow, including the hybrid GFM/TeX Literate Idris.For example: 5b014ec removes some innocent-looking...
\todo[inline]{...}
... calls that broke the PDF build on my system.
Document the workaround
While this is a translation of a book written for/in Coq, we should use idiomatic Idris whenever possible.
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)
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.