Skip to content

Commit 7f4d220

Browse files
committed
Preface: "Proof Assistants" is good enough for now
1 parent cb30cc3 commit 7f4d220

File tree

1 file changed

+1
-3
lines changed

1 file changed

+1
-3
lines changed

src/Preface.lidr

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -109,8 +109,6 @@ propositions. These tools fall into two broad categories:
109109
difficult aspects. Widely used \glspl{proof assistant} include Isabelle,
110110
Agda, Twelf, ACL2, PVS, Coq, and Idris among many others.
111111
112-
\todo[inline]{Edit the following}
113-
114112
This course is based around Idris, a general purpose pure functional programming
115113
language with _dependent types_ that has been under development since 2006 and
116114
that in recent years has attracted a large community of users in both research
@@ -122,7 +120,7 @@ specified precisely in the \gls{type}. On top of this kernel, the Idris
122120
environment provides high-level facilities for proof development, including
123121
powerful tactics for constructing complex proofs semi-automatically, and a large
124122
library of common definitions and lemmas. In some ways, Idris's theorem-proving
125-
is similar to Coq.
123+
is similar to Coq's.
126124

127125
\todo[inline]{Consider comparing Coq and Idris here, or at least qualifying
128126
"some ways"}

0 commit comments

Comments
 (0)