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 02bace9 commit a214fc7Copy full SHA for a214fc7
experiments/idris/src/Fathom/Open/Record.idr
@@ -1,7 +1,7 @@
1
||| Open format universe
2
|||
3
||| This module defines an open universe of binary format descriptions using
4
-||| records to define an inderface. By defining formats in this way, the
+||| records to define an interface. By defining formats in this way, the
5
||| universe of formats is open to extension.
6
7
||| I’m not sure, but this reminds me a little of the ‘coinductive universes’
0 commit comments