Skip to content

Commit

Permalink
re-render html
Browse files Browse the repository at this point in the history
  • Loading branch information
@anton-trunov
anton-trunov committed Jul 7, 2021
1 parent a3a22a8 commit 705b7da
Show file tree
Hide file tree
Showing 10 changed files with 18 additions and 17 deletions.
2 changes: 1 addition & 1 deletion lectures/lecture01.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
<title>The basics of Coq and how to interact with it</title>
<meta name="author" content="Anton Trunov" />
<meta name="date" content="March 11, 2021" />
Expand Down
4 changes: 2 additions & 2 deletions lectures/lecture02.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
<title>Polymorphic functions, parameterized types</title>
<meta name="author" content="Anton Trunov" />
<meta name="date" content="March 18, 2021" />
Expand Down Expand Up @@ -430,7 +430,7 @@ <h2>Notation scopes</h2>
<h1>Sum Type</h1>
<p>The next important type in functional
programming is the sum type. This is also know as
<code class="highlight coq"><span class="name">Result</span></code> type in OCaml or <code class="highlight coq"><span class="name">Maybe</span></code> type in Haskell.</p>
<code class="highlight coq"><span class="name">Result</span></code> type in OCaml or <code class="highlight coq"><span class="name">Either</span></code> type in Haskell.</p>
<pre class="alectryon-io"><!-- Generator: Alectryon --><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Inductive</span> <span class="nf">sum</span> (<span class="nv">A</span> <span class="nv">B</span> : <span class="kt">Type</span>) : <span class="kt">Type</span> :=
| inl of A
| inr of B.</span></span><span class="alectryon-wsp">
Expand Down
2 changes: 1 addition & 1 deletion lectures/lecture03.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
<title>Logic, equality, dependent pattern matching</title>
<meta name="author" content="Anton Trunov" />
<meta name="date" content="March 25, 2021" />
Expand Down
2 changes: 1 addition & 1 deletion lectures/lecture04.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
<title>Injectivity and disjointness of constructors, large elimination. Convoy pattern. Proofs by induction. Prop vs Type</title>
<meta name="author" content="Anton Trunov" />
<meta name="date" content="April 1, 2021" />
Expand Down
2 changes: 1 addition & 1 deletion lectures/lecture05.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
<title>The SSReflect tactic language</title>
<meta name="author" content="Anton Trunov" />
<meta name="date" content="April 8, 2021" />
Expand Down
2 changes: 1 addition & 1 deletion lectures/lecture06.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
<title>Proofs by induction. The SSReflect proof methodology</title>
<meta name="author" content="Anton Trunov" />
<meta name="date" content="April 15, 2021" />
Expand Down
2 changes: 1 addition & 1 deletion lectures/lecture07.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
<title>Views. reflect-predicate. Multi-rewrite rules</title>
<meta name="author" content="Anton Trunov" />
<meta name="date" content="April 22, 2021" />
Expand Down
2 changes: 1 addition & 1 deletion lectures/lecture08_demo.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
<title>lecture08_demo.v</title>
<link rel="stylesheet" href="alectryon.css" type="text/css" />
<link rel="stylesheet" href="docutils_basic.css" type="text/css" />
Expand Down
2 changes: 1 addition & 1 deletion lectures/lecture09.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
<title>lecture09.v</title>
<link rel="stylesheet" href="alectryon.css" type="text/css" />
<link rel="stylesheet" href="docutils_basic.css" type="text/css" />
Expand Down
Loading

0 comments on commit 705b7da

Please sign in to comment.