fixing up versions
This commit is contained in:
wadler
commit
1b6e887f05
4 changed files with 190 additions and 47 deletions
20
Gemfile
20
Gemfile
|
|
@ -1,28 +1,10 @@
|
|||
source "https://rubygems.org"
|
||||
ruby RUBY_VERSION
|
||||
|
||||
# Hello! This is where you manage which Jekyll version is used to run.
|
||||
# When you want to use a different version, change it below, save the
|
||||
# file and run `bundle install`. Run Jekyll with `bundle exec`, like so:
|
||||
#
|
||||
# bundle exec jekyll serve
|
||||
#
|
||||
# This will help ensure the proper Jekyll version is running.
|
||||
# Happy Jekylling!
|
||||
gem "jekyll", "3.4.2"
|
||||
|
||||
# This is the default theme for new Jekyll sites. You may change this to anything you like.
|
||||
gem "minima", "~> 2.0"
|
||||
gem "github-pages", group: :jekyll_plugins
|
||||
|
||||
# If you want to use GitHub Pages, remove the "gem "jekyll"" above and
|
||||
# uncomment the line below. To upgrade, run `bundle update github-pages`.
|
||||
# gem "github-pages", group: :jekyll_plugins
|
||||
|
||||
# If you have any plugins, put them here!
|
||||
group :jekyll_plugins do
|
||||
gem "jekyll-feed", "~> 0.6"
|
||||
end
|
||||
|
||||
# Windows does not include zoneinfo files, so bundle the tzinfo-data gem
|
||||
gem 'tzinfo-data', platforms: [:mingw, :mswin, :x64_mingw, :jruby]
|
||||
|
||||
|
|
|
|||
175
Gemfile.lock
175
Gemfile.lock
|
|
@ -1,12 +1,79 @@
|
|||
GEM
|
||||
remote: https://rubygems.org/
|
||||
specs:
|
||||
addressable (2.5.0)
|
||||
activesupport (4.2.8)
|
||||
i18n (~> 0.7)
|
||||
minitest (~> 5.1)
|
||||
thread_safe (~> 0.3, >= 0.3.4)
|
||||
tzinfo (~> 1.1)
|
||||
addressable (2.5.1)
|
||||
public_suffix (~> 2.0, >= 2.0.2)
|
||||
coffee-script (2.4.1)
|
||||
coffee-script-source
|
||||
execjs
|
||||
coffee-script-source (1.12.2)
|
||||
colorator (1.1.0)
|
||||
ethon (0.10.1)
|
||||
ffi (>= 1.3.0)
|
||||
execjs (2.7.0)
|
||||
faraday (0.12.1)
|
||||
multipart-post (>= 1.2, < 3)
|
||||
ffi (1.9.18)
|
||||
forwardable-extended (2.6.0)
|
||||
jekyll (3.4.2)
|
||||
gemoji (3.0.0)
|
||||
github-pages (140)
|
||||
activesupport (= 4.2.8)
|
||||
github-pages-health-check (= 1.3.4)
|
||||
jekyll (= 3.4.3)
|
||||
jekyll-avatar (= 0.4.2)
|
||||
jekyll-coffeescript (= 1.0.1)
|
||||
jekyll-default-layout (= 0.1.4)
|
||||
jekyll-feed (= 0.9.2)
|
||||
jekyll-gist (= 1.4.0)
|
||||
jekyll-github-metadata (= 2.3.1)
|
||||
jekyll-mentions (= 1.2.0)
|
||||
jekyll-optional-front-matter (= 0.1.2)
|
||||
jekyll-paginate (= 1.1.0)
|
||||
jekyll-readme-index (= 0.1.0)
|
||||
jekyll-redirect-from (= 0.12.1)
|
||||
jekyll-relative-links (= 0.4.0)
|
||||
jekyll-sass-converter (= 1.5.0)
|
||||
jekyll-seo-tag (= 2.2.3)
|
||||
jekyll-sitemap (= 1.0.0)
|
||||
jekyll-swiss (= 0.4.0)
|
||||
jekyll-theme-architect (= 0.0.4)
|
||||
jekyll-theme-cayman (= 0.0.4)
|
||||
jekyll-theme-dinky (= 0.0.4)
|
||||
jekyll-theme-hacker (= 0.0.4)
|
||||
jekyll-theme-leap-day (= 0.0.4)
|
||||
jekyll-theme-merlot (= 0.0.4)
|
||||
jekyll-theme-midnight (= 0.0.4)
|
||||
jekyll-theme-minimal (= 0.0.4)
|
||||
jekyll-theme-modernist (= 0.0.4)
|
||||
jekyll-theme-primer (= 0.2.1)
|
||||
jekyll-theme-slate (= 0.0.4)
|
||||
jekyll-theme-tactile (= 0.0.4)
|
||||
jekyll-theme-time-machine (= 0.0.4)
|
||||
jekyll-titles-from-headings (= 0.1.5)
|
||||
jemoji (= 0.8.0)
|
||||
kramdown (= 1.13.2)
|
||||
liquid (= 3.0.6)
|
||||
listen (= 3.0.6)
|
||||
mercenary (~> 0.3)
|
||||
minima (= 2.1.1)
|
||||
rouge (= 1.11.1)
|
||||
terminal-table (~> 1.4)
|
||||
github-pages-health-check (1.3.4)
|
||||
addressable (~> 2.3)
|
||||
net-dns (~> 0.8)
|
||||
octokit (~> 4.0)
|
||||
public_suffix (~> 2.0)
|
||||
typhoeus (~> 0.7)
|
||||
html-pipeline (2.6.0)
|
||||
activesupport (>= 2)
|
||||
nokogiri (>= 1.4)
|
||||
i18n (0.8.4)
|
||||
jekyll (3.4.3)
|
||||
addressable (~> 2.4)
|
||||
colorator (~> 1.0)
|
||||
jekyll-sass-converter (~> 1.0)
|
||||
|
|
@ -17,41 +84,119 @@ GEM
|
|||
pathutil (~> 0.9)
|
||||
rouge (~> 1.7)
|
||||
safe_yaml (~> 1.0)
|
||||
jekyll-feed (0.9.1)
|
||||
jekyll-avatar (0.4.2)
|
||||
jekyll (~> 3.0)
|
||||
jekyll-coffeescript (1.0.1)
|
||||
coffee-script (~> 2.2)
|
||||
jekyll-default-layout (0.1.4)
|
||||
jekyll (~> 3.0)
|
||||
jekyll-feed (0.9.2)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-gist (1.4.0)
|
||||
octokit (~> 4.2)
|
||||
jekyll-github-metadata (2.3.1)
|
||||
jekyll (~> 3.1)
|
||||
octokit (~> 4.0, != 4.4.0)
|
||||
jekyll-mentions (1.2.0)
|
||||
activesupport (~> 4.0)
|
||||
html-pipeline (~> 2.3)
|
||||
jekyll (~> 3.0)
|
||||
jekyll-optional-front-matter (0.1.2)
|
||||
jekyll (~> 3.0)
|
||||
jekyll-paginate (1.1.0)
|
||||
jekyll-readme-index (0.1.0)
|
||||
jekyll (~> 3.0)
|
||||
jekyll-redirect-from (0.12.1)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-relative-links (0.4.0)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-sass-converter (1.5.0)
|
||||
sass (~> 3.4)
|
||||
jekyll-seo-tag (2.2.3)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-sitemap (1.0.0)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-swiss (0.4.0)
|
||||
jekyll-theme-architect (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-cayman (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-dinky (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-hacker (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-leap-day (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-merlot (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-midnight (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-minimal (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-modernist (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-primer (0.2.1)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-slate (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-tactile (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-theme-time-machine (0.0.4)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-titles-from-headings (0.1.5)
|
||||
jekyll (~> 3.3)
|
||||
jekyll-watch (1.5.0)
|
||||
listen (~> 3.0, < 3.1)
|
||||
jemoji (0.8.0)
|
||||
activesupport (~> 4.0)
|
||||
gemoji (~> 3.0)
|
||||
html-pipeline (~> 2.2)
|
||||
jekyll (>= 3.0)
|
||||
kramdown (1.13.2)
|
||||
liquid (3.0.6)
|
||||
listen (3.0.8)
|
||||
rb-fsevent (~> 0.9, >= 0.9.4)
|
||||
rb-inotify (~> 0.9, >= 0.9.7)
|
||||
listen (3.0.6)
|
||||
rb-fsevent (>= 0.9.3)
|
||||
rb-inotify (>= 0.9.7)
|
||||
mercenary (0.3.6)
|
||||
minima (2.1.0)
|
||||
mini_portile2 (2.2.0)
|
||||
minima (2.1.1)
|
||||
jekyll (~> 3.3)
|
||||
minitest (5.10.2)
|
||||
multipart-post (2.0.0)
|
||||
net-dns (0.8.0)
|
||||
nokogiri (1.8.0)
|
||||
mini_portile2 (~> 2.2.0)
|
||||
octokit (4.7.0)
|
||||
sawyer (~> 0.8.0, >= 0.5.3)
|
||||
pathutil (0.14.0)
|
||||
forwardable-extended (~> 2.6)
|
||||
public_suffix (2.0.5)
|
||||
rb-fsevent (0.9.8)
|
||||
rb-inotify (0.9.8)
|
||||
ffi (>= 0.5.0)
|
||||
rb-inotify (0.9.10)
|
||||
ffi (>= 0.5.0, < 2)
|
||||
rouge (1.11.1)
|
||||
safe_yaml (1.0.4)
|
||||
sass (3.4.23)
|
||||
sass (3.4.24)
|
||||
sawyer (0.8.1)
|
||||
addressable (>= 2.3.5, < 2.6)
|
||||
faraday (~> 0.8, < 1.0)
|
||||
terminal-table (1.8.0)
|
||||
unicode-display_width (~> 1.1, >= 1.1.1)
|
||||
thread_safe (0.3.6)
|
||||
typhoeus (0.8.0)
|
||||
ethon (>= 0.8.0)
|
||||
tzinfo (1.2.3)
|
||||
thread_safe (~> 0.1)
|
||||
unicode-display_width (1.3.0)
|
||||
|
||||
PLATFORMS
|
||||
ruby
|
||||
|
||||
DEPENDENCIES
|
||||
jekyll (= 3.4.2)
|
||||
github-pages
|
||||
jekyll-feed (~> 0.6)
|
||||
minima (~> 2.0)
|
||||
tzinfo-data
|
||||
|
||||
RUBY VERSION
|
||||
ruby 2.4.0p0
|
||||
|
||||
BUNDLED WITH
|
||||
1.14.6
|
||||
1.15.0
|
||||
|
|
|
|||
|
|
@ -4,7 +4,8 @@ layout : page
|
|||
permalink : /Basics
|
||||
---
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<pre class="Agda">
|
||||
|
||||
<a name="113" class="Keyword"
|
||||
>open</a
|
||||
><a name="117"
|
||||
|
|
@ -34,7 +35,8 @@ permalink : /Basics
|
|||
><a name="179" class="Symbol"
|
||||
>)</a
|
||||
>
|
||||
{% endraw %}</pre>
|
||||
|
||||
</pre>
|
||||
|
||||
The functional programming style brings programming closer to
|
||||
simple, everyday mathematics: If a procedure or method has no side
|
||||
|
|
@ -87,7 +89,8 @@ very simple example.
|
|||
The following declaration tells Agda that we are defining
|
||||
a new set of data values -- a *type*.
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<pre class="Agda">
|
||||
|
||||
<a name="2469" class="Keyword"
|
||||
>data</a
|
||||
><a name="2473"
|
||||
|
|
@ -198,7 +201,8 @@ a new set of data values -- a *type*.
|
|||
><a name="2612" href="Basics.html#2474" class="Datatype"
|
||||
>Day</a
|
||||
>
|
||||
{% endraw %}</pre>
|
||||
|
||||
</pre>
|
||||
|
||||
The type is called `day`, and its members are `monday`,
|
||||
`tuesday`, etc. The second and following lines of the definition
|
||||
|
|
@ -207,7 +211,8 @@ can be read "`monday` is a `day`, `tuesday` is a `day`, etc."
|
|||
Having defined `day`, we can write functions that operate on
|
||||
days.
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<pre class="Agda">
|
||||
|
||||
<a name="2894" href="Basics.html#2894" class="Function"
|
||||
>nextWeekday</a
|
||||
><a name="2905"
|
||||
|
|
@ -346,7 +351,8 @@ days.
|
|||
><a name="3135" href="Basics.html#2492" class="InductiveConstructor"
|
||||
>monday</a
|
||||
>
|
||||
{% endraw %}</pre>
|
||||
|
||||
</pre>
|
||||
|
||||
One thing to note is that the argument and return types of
|
||||
this function are explicitly declared. Like most functional
|
||||
|
|
@ -369,7 +375,8 @@ above example to Agda, and observe the result.
|
|||
Second, we can record what we *expect* the result to be in the
|
||||
form of an Agda type:
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<pre class="Agda">
|
||||
|
||||
<a name="4097" href="Basics.html#4097" class="Function Operator"
|
||||
>test_nextWeekday</a
|
||||
><a name="4113"
|
||||
|
|
@ -401,7 +408,8 @@ form of an Agda type:
|
|||
><a name="4153" href="Basics.html#2510" class="InductiveConstructor"
|
||||
>tuesday</a
|
||||
>
|
||||
{% endraw %}</pre>
|
||||
|
||||
</pre>
|
||||
|
||||
This declaration does two things: it makes an assertion (that the second
|
||||
weekday after `saturday` is `tuesday`), and it gives the assertion a name
|
||||
|
|
@ -410,7 +418,8 @@ that can be used to refer to it later.
|
|||
Having made the assertion, we must also verify it. We do this by giving
|
||||
a term of the above type:
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<pre class="Agda">
|
||||
|
||||
<a name="4472" href="Basics.html#4097" class="Function Operator"
|
||||
>test_nextWeekday</a
|
||||
><a name="4488"
|
||||
|
|
@ -422,7 +431,8 @@ a term of the above type:
|
|||
><a name="4491" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
|
||||
>refl</a
|
||||
>
|
||||
{% endraw %}</pre>
|
||||
|
||||
</pre>
|
||||
|
||||
There is no essential difference between the definition for
|
||||
`test_nextWeekday` here and the definition for `nextWeekday` above,
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ a nice case study using ideas we've seen in previous chapters, including
|
|||
building data structures out of higher-order functions (from [Basics]({{
|
||||
"Basics" | relative_url }}) and [Poly]({{ "Poly" | relative_url }}) and the use
|
||||
of reflection to streamline proofs (from [IndProp]({{ "IndProp" | relative_url
|
||||
}})).
|
||||
}})).
|
||||
|
||||
We'll define two flavors of maps: _total_ maps, which include a
|
||||
"default" element to be returned when a key being looked up
|
||||
|
|
@ -64,7 +64,7 @@ contrapositive : ∀ {ℓ₁ ℓ₂} {P : Set ℓ₁} {Q : Set ℓ₂} → (P
|
|||
contrapositive p→q ¬q p = ¬q (p→q p)
|
||||
\end{code}
|
||||
|
||||
Using the above, we can decide equality of two identifiers
|
||||
Using the above, we can decide equality of two identifiers
|
||||
by deciding equality on the underlying strings.
|
||||
|
||||
\begin{code}
|
||||
|
|
@ -143,6 +143,12 @@ function that behaves like the desired map.
|
|||
|
||||
We define handy abbreviations for updating a map two, three, or four times.
|
||||
|
||||
<div class="note hidden">
|
||||
Wen: you don't actually need to define these, you can simply declare `_,_↦_` to
|
||||
be a left-associative infix operator with an `infixl` statement, and then you'll
|
||||
be able to just evaluate `M , x ↦ y , z ↦ w` as `(M , x ↦ y) , z ↦ w`.
|
||||
</div>
|
||||
|
||||
\begin{code}
|
||||
_,_↦_,_↦_ : ∀ {A} → TotalMap A → Id → A → Id → A → TotalMap A
|
||||
ρ , x₁ ↦ v₁ , x₂ ↦ v₂ = (ρ , x₁ ↦ v₁), x₂ ↦ v₂
|
||||
|
|
@ -180,7 +186,7 @@ application!
|
|||
To use maps in later chapters, we'll need several fundamental
|
||||
facts about how they behave. Even if you don't work the following
|
||||
exercises, make sure you understand the statements of
|
||||
the lemmas!
|
||||
the lemmas!
|
||||
|
||||
#### Exercise: 1 star, optional (apply-always)
|
||||
The `always` map returns its default element for all keys:
|
||||
|
|
|
|||
Loading…
Reference in a new issue