We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 9a0035c commit 348bd7fCopy full SHA for 348bd7f
src/ProofObjects.lidr
@@ -2,8 +2,8 @@
2
3
> module ProofObjects
4
5
-\say{"\textit{Algorithms are the computational content of proofs.}" - Robert
6
-Harper}
+\say{\textit{Algorithms are the computational content of proofs.}}
+-- Robert Harper
7
8
We have seen that Idris has mechanisms both for _programming_, using inductive
9
data types like \idr{Nat} or \idr{List} and functions over these types, and for
0 commit comments