From c84c1e84a517c4a117117cab0229012af627460f Mon Sep 17 00:00:00 2001 From: gallais Date: Sun, 24 Dec 2023 11:23:09 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20ohad/col?= =?UTF-8?q?lie@e496277f6dd557d31668b2430cfb07c47e841e2f=20=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- alternative.css | 247 +++++++++++++++++ blackandwhite.css | 248 ++++++++++++++++++ styles.css => default.css | 13 +- docs/Collie.Core.html | 65 ++++- docs/Collie.Error.html | 65 ++++- docs/Collie.Modifiers.html | 65 ++++- docs/Collie.Options.Domain.html | 65 ++++- docs/Collie.Options.Usual.html | 65 ++++- docs/Collie.Parser.html | 65 ++++- docs/Collie.Usage.html | 65 ++++- docs/Collie.html | 70 ++++- docs/Data.List.Fresh.Elem.html | 65 ++++- ...t.Fresh.Quantifiers.SmartConstructors.html | 65 ++++- docs/Data.List.Fresh.Quantifiers.html | 65 ++++- docs/Data.List.Fresh.html | 75 +++++- docs/Data.Magma.html | 65 ++++- docs/Data.Record.SmartConstructors.html | 68 ++++- docs/Data.Record.html | 69 ++++- docs/Decidable.Decidable.Extra1.html | 65 ++++- index.html | 65 ++++- 20 files changed, 1602 insertions(+), 33 deletions(-) create mode 100644 alternative.css create mode 100644 blackandwhite.css rename styles.css => default.css (95%) diff --git a/alternative.css b/alternative.css new file mode 100644 index 0000000..58882e9 --- /dev/null +++ b/alternative.css @@ -0,0 +1,247 @@ +html, +body { + margin: 0; + padding: 0; + border: 0; + height: 100%; + font-family: "Trebuchet MS", Helvetica, sans-serif; + font-size: 11pt; + background-color: #fff; +} + +a, +a:active, +a:visited { + text-decoration: none; + color: inherit; +} + +a:hover { + text-decoration: underline; +} + +header { + padding: 5px 11px; + border-bottom: 3px solid #659fdb; + box-shadow: 0 -8px 22px 0; + background-color: #252525; + color: white; + font-size: 9pt; +} + +.wrapper { + min-height: 100%; +} + +header nav, +header strong { + font-size: 11pt; +} + +header nav { + float: right; +} + +footer { + height: 30px; + width: 100%; + border-top: 1px solid #aaa; + margin-top: -31px; + text-align: center; + color: #666; + line-height: 30px; + font-size: 9pt; + background: none repeat scroll 0 0 #ddd; +} + +.container { + padding: 10px 10px 41px 20px; +} + +h1 { + margin: 0; + margin-bottom: 5px; + font-size: 14pt; + font-family: "Trebuchet MS", Helvetica, sans-serif; +} + +#module-header { + border-bottom: 1px solid #bbb; + padding-bottom: 2px; +} + +ul { + list-style-type: none; + margin: 0; + padding: 0; +} + +hr { + margin: 0; + padding: 0; + border: 0; + border-bottom: 1px solid #bbb; +} + +p { + margin: 0; + padding: 0; +} + +pre { + display: inline; + margin: 0; + padding: 0; +} + +.code { + font-family: "Lucida Console", Monaco, monospace; + font-size: 10pt; +} + +.decls { + margin-top: 5px; +} + +.decls > dt { + font-family: "Lucida Console", Monaco, monospace; + font-size: 10pt; + line-height: 20px; + padding: 2px 6px; + border: 1px solid #ccc; + background-color: #f0f0f0; + display: table; + width: 100%; + box-sizing: border-box; + white-space: pre-wrap; +} + +.decls > dd { + margin: 10px 0 20px 20px; + font-family: Arial, sans-serif; + font-size: 10pt; +} + +.decls > dd > p { + margin-bottom: 8px; +} + +.decls > dd > dl:not(.decls):not(:first-child) { + padding-top: 5px; + border-top: 1px solid #eee; +} + +.decls > dd > dl:not(.decls) > dt { + display: block; + min-width: 70px; + float: left; + font-weight: bold; +} + +.decls > dd > dl:not(.decls) > dd { + margin-bottom: 2px; +} + +.fixity { + font-style: italic; + font-weight: normal !important; +} + +dd.fixity { + cursor: default; +} + +.word { + display: table-cell; + white-space: nowrap; + width: 0; +} + +.signature { + display: table-cell; + width: 100%; +} + +.name { + white-space: nowrap; + width: 0; +} + +.documented, +.name { + cursor: default; +} + +.documented { + font-weight: bold; +} + +/* The following colours are taken from the conservative 8 color palette given + in http://mkweb.bcgsc.ca/colorblind/palettes.mhtml +*/ + +a.function { + color: #359b73; +} + +.function { + color: #359b73; +} + +a.constructor { + color: #d55e; +} + +.constructor { + color: #d55e; +} + +a.type { + color: #3db7e9; +} + +.type { + color: #3db7e9; +} + +.keyword { + color: inherit; +} + +.boundvar { + color: #f748a5; +} + +.boundvar.implicit { + text-decoration: underline; +} + +ul.names { + border: 1px solid #666; +} + +ul.names li { + padding-left: 5px; +} + +ul.names li a { + display: inline-block; + width: 100%; + padding: 2px 0; +} + +ul.names li:nth-child(odd) { + background-color: #eeeeef; +} + +ul.names li:nth-child(even) { + background-color: white; +} + +body.index .container a:visited { + color: #666; +} + +body.index .container a:hover { + color: #04819e; +} diff --git a/blackandwhite.css b/blackandwhite.css new file mode 100644 index 0000000..3486cbf --- /dev/null +++ b/blackandwhite.css @@ -0,0 +1,248 @@ +html, +body { + margin: 0; + padding: 0; + border: 0; + height: 100%; + font-family: "Trebuchet MS", Helvetica, sans-serif; + font-size: 11pt; + background-color: #fff; +} + +a, +a:active, +a:visited { + text-decoration: none; + color: inherit; +} + +a:hover { + text-decoration: underline; +} + +header { + padding: 5px 11px; + border-bottom: 3px solid #659fdb; + box-shadow: 0 -8px 22px 0; + background-color: #252525; + color: white; + font-size: 9pt; +} + +.wrapper { + min-height: 100%; +} + +header nav, +header strong { + font-size: 11pt; +} + +header nav { + float: right; +} + +footer { + height: 30px; + width: 100%; + border-top: 1px solid #aaa; + margin-top: -31px; + text-align: center; + color: #666; + line-height: 30px; + font-size: 9pt; + background: none repeat scroll 0 0 #ddd; +} + +.container { + padding: 10px 10px 41px 20px; +} + +h1 { + margin: 0; + margin-bottom: 5px; + font-size: 14pt; + font-family: "Trebuchet MS", Helvetica, sans-serif; +} + +#module-header { + border-bottom: 1px solid #bbb; + padding-bottom: 2px; +} + +ul { + list-style-type: none; + margin: 0; + padding: 0; +} + +hr { + margin: 0; + padding: 0; + border: 0; + border-bottom: 1px solid #bbb; +} + +p { + margin: 0; + padding: 0; +} + +pre { + display: inline; + margin: 0; + padding: 0; +} + +.code { + font-family: "Lucida Console", Monaco, monospace; + font-size: 10pt; +} + +.decls { + margin-top: 5px; +} + +.decls > dt { + font-family: "Lucida Console", Monaco, monospace; + font-size: 10pt; + line-height: 20px; + padding: 2px 6px; + border: 1px solid #ccc; + background-color: #f0f0f0; + display: table; + width: 100%; + box-sizing: border-box; + white-space: pre-wrap; +} + +.decls > dd { + margin: 10px 0 20px 20px; + font-family: Arial, sans-serif; + font-size: 10pt; +} + +.decls > dd > p { + margin-bottom: 8px; +} + +.decls > dd > dl:not(.decls):not(:first-child) { + padding-top: 5px; + border-top: 1px solid #eee; +} + +.decls > dd > dl:not(.decls) > dt { + display: block; + min-width: 70px; + float: left; + font-weight: bold; +} + +.decls > dd > dl:not(.decls) > dd { + margin-bottom: 2px; +} + +.fixity { + font-style: italic; + font-weight: normal !important; +} + +dd.fixity { + cursor: default; +} + +.word { + display: table-cell; + white-space: nowrap; + width: 0; +} + +.signature { + display: table-cell; + width: 100%; +} + +.name { + white-space: nowrap; + width: 0; +} + +.documented, +.name { + cursor: default; + font-weight: normal; + font-style: normal; + font-variant: normal; +} + +.documented { + font-weight: bold; +} + +a.function { + font-style: italic; +} + +.function { + font-style: italic; +} + +a.constructor { + font-weight: bold; +} + +.constructor { + font-weight: bold; +} + +a.type { + font-variant: small-caps !important; +} + +.type { + font-variant: small-caps !important; +} + +.keyword { + text-decoration: underline; + color: inherit; +} + +.boundvar { + color: #bf30bf; /* Too much colour makes it hard to differ the rest of the colours */ + color: inherit; +} + +.boundvar.implicit { + text-decoration: underline; +} + +ul.names { + border: 1px solid #666; +} + +ul.names li { + padding-left: 5px; +} + +ul.names li a { + display: inline-block; + width: 100%; + padding: 2px 0; +} + +ul.names li:nth-child(odd) { + background-color: #eeeeef; +} + +ul.names li:nth-child(even) { + background-color: white; +} + +body.index .container a:visited { + color: #666; +} + +body.index .container a:hover { + color: #04819e; +} diff --git a/styles.css b/default.css similarity index 95% rename from styles.css rename to default.css index 916ca7c..306aaea 100644 --- a/styles.css +++ b/default.css @@ -65,7 +65,7 @@ h1 { font-family: "Trebuchet MS", Helvetica, sans-serif; } -#moduleHeader { +#module-header { border-bottom: 1px solid #bbb; padding-bottom: 2px; } @@ -88,6 +88,12 @@ p { padding: 0; } +pre { + display: inline; + margin: 0; + padding: 0; +} + .code { font-family: "Lucida Console", Monaco, monospace; font-size: 10pt; @@ -195,12 +201,11 @@ a.type { } .keyword { - color: inherit; + color: #999; } .boundvar { - color: #bf30bf; /* Too much colour makes it hard to differ the rest of the colours */ - color: inherit; + color: #bf30bf; } .boundvar.implicit { diff --git a/docs/Collie.Core.html b/docs/Collie.Core.html index 75b7ee7..d394bd4 100644 --- a/docs/Collie.Core.html +++ b/docs/Collie.Core.html @@ -1 +1,64 @@ -Collie.Core
Idris2Doc : Collie.Core

Collie.Core

data Any : ((0 nm : String) -> Command nm -> Type) -> Command nm -> Type
Totality: total
Constructors:
Here : p nm cmd -> Any p cmd
There : (pos : IsField c (cmd .subcommands)) -> Any p (snd (field pos)) -> Any p cmd
record Command : String -> Type
Totality: total
Constructor: 
MkCommand : String -> Fields Command -> Fields Modifier -> Arguments -> Command name

Projections:
arguments : Command name -> Arguments
description : Command name -> String
modifiers : Command name -> Fields Modifier
subcommands : Command name -> Fields Command
ParseTree : Command nm -> Type
Totality: total
ParseTreeT : (Type -> Type) -> (Type -> Type) -> Command nm -> Type
Totality: total
record ParsedCommand : (0 nm : String) -> Command nm -> Type
Totality: total
Constructor: 
MkParsedCommand : ParsedModifiers (cmd .modifiers) -> ParsedArguments (cmd .arguments) -> ParsedCommand nm cmd

Projections:
arguments : ParsedCommand nm cmd -> ParsedArguments (cmd .arguments)
modifiers : ParsedCommand nm cmd -> ParsedModifiers (cmd .modifiers)
record ParsedCommandT : (Type -> Type) -> (Type -> Type) -> (0 nm : String) -> Command nm -> Type
Totality: total
Constructor: 
MkParsedCommandT : ParsedModifiersT f g (cmd .modifiers) -> ParsedArgumentsT g (cmd .arguments) -> ParsedCommandT f g nm cmd

Projections:
arguments : ParsedCommandT f g nm cmd -> ParsedArgumentsT g (cmd .arguments)
modifiers : ParsedCommandT f g nm cmd -> ParsedModifiersT f g (cmd .modifiers)
basic : String -> Arguments -> Command cmdName
Totality: total
initParsedCommand : ParsedCommandT Maybe Maybe nm cmd
Totality: total
lookup : Any p c -> DPair String (\nm => Command nm)
Totality: total
\ No newline at end of file + + + + + Collie.Core + + + + + +
+ Idris2Doc : Collie.Core + + + + +
+

Collie.Core

Reexports
import public Collie.Options.Domain
import public Collie.Options.Usual
import public Collie.Modifiers
import public Data.Record
import public Data.Record.SmartConstructors
import public Data.Vect
import public Data.DPair
import public Data.Magma
import public Syntax.WithProof
import public Decidable.Decidable
import public Decidable.Decidable.Extra1
Definitions
record Command : String -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCommand : String -> Fields Command -> Fields Modifier -> Arguments -> Command name

  Projections:
  
.arguments : Command name -> Arguments
  
.description : Command name -> String
  
.modifiers : Command name -> Fields Modifier
  
.subcommands : Command name -> Fields Command
.description : Command name -> String
  Totality: total
  Visibility: public export
description : Command name -> String
  Totality: total
  Visibility: public export
.subcommands : Command name -> Fields Command
  Totality: total
  Visibility: public export
subcommands : Command name -> Fields Command
  Totality: total
  Visibility: public export
.modifiers : Command name -> Fields Modifier
  Totality: total
  Visibility: public export
modifiers : Command name -> Fields Modifier
  Totality: total
  Visibility: public export
.arguments : Command name -> Arguments
  Totality: total
  Visibility: public export
arguments : Command name -> Arguments
  Totality: total
  Visibility: public export
basic : String -> Arguments -> Command cmdName
  Totality: total
  Visibility: public export
data Any : ((0 nm : String) -> Command nm -> Type) -> Command nm -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Here : p nm cmd -> Any p cmd
  
There : (pos : IsField c (cmd .subcommands)) -> Any p (snd (field pos)) -> Any p cmd
map : ((cmd : Command nm) -> p nm cmd -> q nm cmd) -> Any p cmd -> Any q cmd
  Totality: total
  Visibility: public export
traverse : Applicative m => ((cmd : Command nm) -> p nm cmd -> m (q nm cmd)) -> Any p cmd -> m (Any q cmd)
  Totality: total
  Visibility: public export
record ParsedCommandT : (Type -> Type) -> (Type -> Type) -> (0 nm : String) -> Command nm -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkParsedCommandT : ParsedModifiersT f g (cmd .modifiers) -> ParsedArgumentsT g (cmd .arguments) -> ParsedCommandT f g nm cmd

  Projections:
  
.arguments : ParsedCommandT f g nm cmd -> ParsedArgumentsT g (cmd .arguments)
  
.modifiers : ParsedCommandT f g nm cmd -> ParsedModifiersT f g (cmd .modifiers)
.modifiers : ParsedCommandT f g nm cmd -> ParsedModifiersT f g (cmd .modifiers)
  Totality: total
  Visibility: public export
modifiers : ParsedCommandT f g nm cmd -> ParsedModifiersT f g (cmd .modifiers)
  Totality: total
  Visibility: public export
.arguments : ParsedCommandT f g nm cmd -> ParsedArgumentsT g (cmd .arguments)
  Totality: total
  Visibility: public export
arguments : ParsedCommandT f g nm cmd -> ParsedArgumentsT g (cmd .arguments)
  Totality: total
  Visibility: public export
record ParsedCommand : (0 nm : String) -> Command nm -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkParsedCommand : ParsedModifiers (cmd .modifiers) -> ParsedArguments (cmd .arguments) -> ParsedCommand nm cmd

  Projections:
  
.arguments : ParsedCommand nm cmd -> ParsedArguments (cmd .arguments)
  
.modifiers : ParsedCommand nm cmd -> ParsedModifiers (cmd .modifiers)
.modifiers : ParsedCommand nm cmd -> ParsedModifiers (cmd .modifiers)
  Totality: total
  Visibility: public export
modifiers : ParsedCommand nm cmd -> ParsedModifiers (cmd .modifiers)
  Totality: total
  Visibility: public export
.arguments : ParsedCommand nm cmd -> ParsedArguments (cmd .arguments)
  Totality: total
  Visibility: public export
arguments : ParsedCommand nm cmd -> ParsedArguments (cmd .arguments)
  Totality: total
  Visibility: public export
defaulting : ParsedCommandT Maybe f nm cmd -> ParsedCommandT id f nm cmd
  Totality: total
  Visibility: public export
finalising : ParsedCommandT Maybe Maybe nm cmd -> Error (ParsedCommand nm cmd)
  Totality: total
  Visibility: public export
ParseTreeT : (Type -> Type) -> (Type -> Type) -> Command nm -> Type
  Totality: total
  Visibility: public export
ParseTree : Command nm -> Type
  Totality: total
  Visibility: public export
defaulting : ParseTreeT Maybe f cmd -> ParseTreeT id f cmd
  Totality: total
  Visibility: public export
finalising : ParseTreeT Maybe Maybe cmd -> Error (ParseTree cmd)
  Totality: total
  Visibility: public export
lookup : Any p c -> (nm : String ** Command nm)
  Totality: total
  Visibility: public export
.update : ParsedArgumentsT Maybe arg -> String -> Error (ParsedArgumentsT Maybe arg)
  Totality: total
  Visibility: public export
.parse : (args : Arguments) -> ParsedArgumentsT Maybe args -> List String -> Error (ParsedArgumentsT Maybe args)
  Totality: total
  Visibility: public export
initParsedCommand : ParsedCommandT Maybe Maybe nm cmd
  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Collie.Error.html b/docs/Collie.Error.html
index 59fac54..d35114c 100644
--- a/docs/Collie.Error.html
+++ b/docs/Collie.Error.html
@@ -1 +1,64 @@
-Collie.Error
Idris2Doc : Collie.Error
Collie.Error
(>>=) : Error a -> (a -> Error b) -> Error b
  Totality: total
  Fixity Declaration: infixl operator, level 1
data Error : Type -> Type
  Totality: total
  Constructors:
  
Fail : List1 ErrorMsg -> Error a
  
Pure : a -> Error a
data ErrorMsg : Type
  Totality: total
  Constructors:
  
CouldNotParse : String -> ErrorMsg
  
MissingOption : String -> ErrorMsg
  
MissingArgument : ErrorMsg
  
OptionSetTwice : String -> ErrorMsg
  
TooManyArguments : ErrorMsg
  
MissingOptArg : String -> ErrorMsg
exitWith : List1 ErrorMsg -> IO a
  Totality: total
fromEither : Either ErrorMsg a -> Error a
  Totality: total
throwE : ErrorMsg -> Error a
  Totality: total

\ No newline at end of file
+
+
+
+  
+  Collie.Error
+  
+  
+
+
+
+

+  Idris2Doc : Collie.Error
+  
+
+  
+
+

+
Collie.Error
Definitions
data ErrorMsg : Type
  Totality: total
  Visibility: public export
  Constructors:
  
CouldNotParse : String -> ErrorMsg
  
MissingOption : String -> ErrorMsg
  
MissingArgument : ErrorMsg
  
OptionSetTwice : String -> ErrorMsg
  
TooManyArguments : ErrorMsg
  
MissingOptArg : String -> ErrorMsg

  Hint: 
Show ErrorMsg
data Error : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Fail : List1 ErrorMsg -> Error a
  
Pure : a -> Error a

  Hints:
  
Applicative Error
  
Functor Error
  
Show a => Show (Error a)
throwE : ErrorMsg -> Error a
  Totality: total
  Visibility: export
fromEither : Either ErrorMsg a -> Error a
  Totality: total
  Visibility: export
(>>=) : Error a -> (a -> Error b) -> Error b
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 1
exitWith : List1 ErrorMsg -> IO a
  Totality: total
  Visibility: export

\ No newline at end of file
diff --git a/docs/Collie.Modifiers.html b/docs/Collie.Modifiers.html
index 353917f..d85e3ee 100644
--- a/docs/Collie.Modifiers.html
+++ b/docs/Collie.Modifiers.html
@@ -1 +1,64 @@
-Collie.Modifiers
Idris2Doc : Collie.Modifiers
Collie.Modifiers
(::=) : {0 a : String -> Type} -> (nm : String) -> a nm -> DPair String (\nm => a nm)
  Totality: total
  Fixity Declaration: infix operator, level 1
Flag : Fields (const Type)
  Totality: total
data Modifier : String -> Type
  Totality: total
  Constructors:
  
MkFlag : Record snd Flag -> Modifier nm
  
MkOption : Record snd Option -> Modifier nm
Option : Fields (const Type)
  Totality: total
ParsedModifier : Modifier nm -> Type
  Totality: total
ParsedModifierT : (Type -> Type) -> (Type -> Type) -> Modifier nm -> Type
  Totality: total
ParsedModifiers : Fields Modifier -> Type
  Totality: total
ParsedModifiersT : (Type -> Type) -> (Type -> Type) -> Fields Modifier -> Type
  Totality: total
defaulting : ParsedModifiersT Maybe f mods -> ParsedModifiersT id f mods
  All the flags have a default value. If no value has been set then use
  that default instead.
  Totality: total
finalising : ParsedModifiersT Maybe Maybe mods -> Error (ParsedModifiers mods)
  Setting the flags to their default value and ensuring that the required
  options are passed.
  Totality: total
flag : String -> {default False _ : Bool} -> Modifier nm
  Totality: total
initNothing : ParsedModifiersT Maybe Maybe flds
  Totality: total
option : String -> Arguments -> Modifier nm
  Totality: total
updateModifier : ParsedModifierT id id mod -> ParsedModifierT Maybe Maybe mod -> Error (ParsedModifierT Maybe Maybe mod)
  Totality: total

\ No newline at end of file
+
+
+
+  
+  Collie.Modifiers
+  
+  
+
+
+
+

+  Idris2Doc : Collie.Modifiers
+  
+
+  
+
+

+
Collie.Modifiers
Reexports
import public Data.Record
import public Collie.Options.Domain
import public Collie.Error
Definitions
(::=) : {0 a : String -> Type} -> (nm : String) -> a nm -> (nm : String ** a nm)
  Totality: total
  Visibility: public export
  Fixity Declarations:
  infix operator, level 1
infix operator, level 1
infix operator, level 4
Flag : Fields (const Type)
  Totality: total
  Visibility: public export
Option : Fields (const Type)
  Totality: total
  Visibility: public export
data Modifier : String -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
MkFlag : Record snd Flag -> Modifier nm
  
MkOption : Record snd Option -> Modifier nm
flag : String -> {default False _ : Bool} -> Modifier nm
  Totality: total
  Visibility: public export
option : String -> Arguments -> Modifier nm
  Totality: total
  Visibility: public export
ParsedModifierT : (Type -> Type) -> (Type -> Type) -> Modifier nm -> Type
  Totality: total
  Visibility: public export
ParsedModifier : Modifier nm -> Type
  Totality: total
  Visibility: public export
ParsedModifiersT : (Type -> Type) -> (Type -> Type) -> Fields Modifier -> Type
  Totality: total
  Visibility: public export
ParsedModifiers : Fields Modifier -> Type
  Totality: total
  Visibility: public export
updateModifier : ParsedModifierT id id mod -> ParsedModifierT Maybe Maybe mod -> Error (ParsedModifierT Maybe Maybe mod)
  Totality: total
  Visibility: public export
.update : ParsedModifiersT Maybe Maybe mods -> (pos : Any p mods) -> ParsedModifierT id id (snd (field pos)) -> Error (ParsedModifiersT Maybe Maybe mods)
  Totality: total
  Visibility: public export
defaulting : ParsedModifiersT Maybe f mods -> ParsedModifiersT id f mods
  All the flags have a default value. If no value has been set then use
  that default instead.

  Totality: total
  Visibility: public export
finalising : Lazy ErrorMsg -> (args : Arguments) -> ParsedArgumentsT Maybe args -> Error (ParsedArguments args)
  Totality: total
  Visibility: public export
finalising : (mod : Modifier nm) -> ParsedModifierT Maybe Maybe mod -> Error (ParsedModifier mod)
  Totality: total
  Visibility: public export
finalising : ParsedModifiersT Maybe Maybe mods -> Error (ParsedModifiers mods)
  Setting the flags to their default value and ensuring that the required
  options are passed.

  Totality: total
  Visibility: public export
initNothing : ParsedModifiersT Maybe Maybe flds
  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Collie.Options.Domain.html b/docs/Collie.Options.Domain.html
index 4ad12bc..703d0b5 100644
--- a/docs/Collie.Options.Domain.html
+++ b/docs/Collie.Options.Domain.html
@@ -1 +1,64 @@
-Collie.Options.Domain
Idris2Doc : Collie.Options.Domain
Collie.Options.Domain
record Arguments : Type
  Totality: total
  Constructor: 
MkArguments : Bool -> (domain : Domain) -> Parser domain -> Arguments

  Projections:
  
domain : Arguments -> Domain
  
rawParser : (rec : Arguments) -> Parser (domain rec)
  
required : Arguments -> Bool
Carrier : Domain -> Type
  Totality: total
data Domain : Type
  Totality: total
  Constructors:
  
Some : Type -> Domain
  
ALot : RawMagma -> Domain
ParsedArguments : Arguments -> Type
  Totality: total
ParsedArgumentsT : (Type -> Type) -> Arguments -> Type
  Totality: total
Parser : Domain -> Type
  Totality: total
elimDomain : {p : Domain -> Type} -> ((d : Type) -> p (Some d)) -> ((ds : RawMagma) -> p (ALot ds)) -> (d : Domain) -> p d
  Totality: total

\ No newline at end of file
+
+
+
+  
+  Collie.Options.Domain
+  
+  
+
+
+
+

+  Idris2Doc : Collie.Options.Domain
+  
+
+  
+
+

+
Collie.Options.Domain
Definitions
data Domain : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Some : Type -> Domain
  
ALot : RawMagma -> Domain
elimDomain : {p : Domain -> Type} -> ((d : Type) -> p (Some d)) -> ((ds : RawMagma) -> p (ALot ds)) -> (d : Domain) -> p d
  Totality: total
  Visibility: public export
Carrier : Domain -> Type
  Totality: total
  Visibility: public export
Parser : Domain -> Type
  Totality: total
  Visibility: public export
record Arguments : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkArguments : Bool -> (domain : Domain) -> Parser domain -> Arguments

  Projections:
  
.domain : Arguments -> Domain
  
.rawParser : ({rec:0} : Arguments) -> Parser (domain {rec:0})
  
.required : Arguments -> Bool
.required : Arguments -> Bool
  Totality: total
  Visibility: public export
required : Arguments -> Bool
  Totality: total
  Visibility: public export
.domain : Arguments -> Domain
  Totality: total
  Visibility: public export
domain : Arguments -> Domain
  Totality: total
  Visibility: public export
.rawParser : ({rec:0} : Arguments) -> Parser (domain {rec:0})
  Totality: total
  Visibility: public export
rawParser : ({rec:0} : Arguments) -> Parser (domain {rec:0})
  Totality: total
  Visibility: public export
.parser : (arg : Arguments) -> String -> Error (Carrier (arg .domain))
  Totality: total
  Visibility: public export
ParsedArgumentsT : (Type -> Type) -> Arguments -> Type
  Totality: total
  Visibility: public export
ParsedArguments : Arguments -> Type
  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Collie.Options.Usual.html b/docs/Collie.Options.Usual.html
index ccfe8dd..32b3eaf 100644
--- a/docs/Collie.Options.Usual.html
+++ b/docs/Collie.Options.Usual.html
@@ -1 +1,64 @@
-Collie.Options.Usual
Idris2Doc : Collie.Options.Usual
Collie.Options.Usual
FilePath : Type
  Totality: total
Regex : Type
  Totality: total
Regexp : Type
  Totality: total
Url : Type
  Totality: total
filePath : Arguments
  Totality: total
integer : Arguments
  Totality: total
lotsOf : Arguments -> Arguments
  Totality: total
nat : Arguments
  Totality: total
none : Arguments
  Totality: total
regex : Arguments
  Totality: total
regexp : Arguments
  Totality: total
url : Arguments
  Totality: total

\ No newline at end of file
+
+
+
+  
+  Collie.Options.Usual
+  
+  
+
+
+
+

+  Idris2Doc : Collie.Options.Usual
+  
+
+  
+
+

+
Collie.Options.Usual
Definitions
none : Arguments
  Totality: total
  Visibility: public export
lotsOf : Arguments -> Arguments
  Totality: total
  Visibility: public export
Regex : Type
  Totality: total
  Visibility: public export
regex : Arguments
  Totality: total
  Visibility: public export
FilePath : Type
  Totality: total
  Visibility: public export
filePath : Arguments
  Totality: total
  Visibility: public export
Regexp : Type
  Totality: total
  Visibility: public export
regexp : Arguments
  Totality: total
  Visibility: public export
Url : Type
  Totality: total
  Visibility: public export
url : Arguments
  Totality: total
  Visibility: public export
nat : Arguments
  Totality: total
  Visibility: public export
integer : Arguments
  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Collie.Parser.html b/docs/Collie.Parser.html
index 4e9ef48..3cd863c 100644
--- a/docs/Collie.Parser.html
+++ b/docs/Collie.Parser.html
@@ -1 +1,64 @@
-Collie.Parser
Idris2Doc : Collie.Parser
Collie.Parser
parse : (cmd : Command nm) -> List String -> Error (ParseTreeT Maybe Maybe cmd)
  Totality: total
parseCommand : (cmd : Command nm) -> List String -> ParsedCommandT Maybe Maybe nm cmd -> Error (ParsedCommandT Maybe Maybe nm cmd)
  Totality: total
parseModifier : (cmd : Command nm) -> (pos : IsField modName (cmd .modifiers)) -> List String -> ParsedCommandT Maybe Maybe nm cmd -> (ParsedModifierT id id (snd (field pos)) -> Error (ParsedModifiersT Maybe Maybe (cmd .modifiers))) -> Error (ParsedCommandT Maybe Maybe nm cmd)
  Totality: total

\ No newline at end of file
+
+
+
+  
+  Collie.Parser
+  
+  
+
+
+
+

+  Idris2Doc : Collie.Parser
+  
+
+  
+
+

+
Collie.Parser
Definitions
parseCommand : (cmd : Command nm) -> List String -> ParsedCommandT Maybe Maybe nm cmd -> Error (ParsedCommandT Maybe Maybe nm cmd)
  Totality: total
  Visibility: public export
parseModifier : (cmd : Command nm) -> (pos : IsField modName (cmd .modifiers)) -> List String -> ParsedCommandT Maybe Maybe nm cmd -> (ParsedModifierT id id (snd (field pos)) -> Error (ParsedModifiersT Maybe Maybe (cmd .modifiers))) -> Error (ParsedCommandT Maybe Maybe nm cmd)
  Totality: total
  Visibility: public export
parse : (cmd : Command nm) -> List String -> Error (ParseTreeT Maybe Maybe cmd)
  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Collie.Usage.html b/docs/Collie.Usage.html
index d6264a4..bd4370f 100644
--- a/docs/Collie.Usage.html
+++ b/docs/Collie.Usage.html
@@ -1 +1,64 @@
-Collie.Usage
Idris2Doc : Collie.Usage
Collie.Usage
Printer : Type
  Totality: total
namedBlock : String -> String -> Nat -> Nat -> Printer
  Totality: total
usageCommand : Command cmdName -> Nat -> Nat -> Printer
  Totality: total
usageModifiers : Fields Modifier -> Nat -> Nat -> Printer
  Totality: total

\ No newline at end of file
+
+
+
+  
+  Collie.Usage
+  
+  
+
+
+
+

+  Idris2Doc : Collie.Usage
+  
+
+  
+
+

+
Collie.Usage
Definitions
Printer : Type
  Totality: total
  Visibility: public export
namedBlock : String -> String -> Nat -> Nat -> Printer
  Totality: total
  Visibility: export
usageModifiers : Fields Modifier -> Nat -> Nat -> Printer
  Totality: total
  Visibility: export
usageCommand : Command cmdName -> Nat -> Nat -> Printer
  Totality: total
  Visibility: export
.usage : {default 80 _ : Nat} -> Command cmdName -> String
  Totality: total
  Visibility: export

\ No newline at end of file
diff --git a/docs/Collie.html b/docs/Collie.html
index 0085424..502261e 100644
--- a/docs/Collie.html
+++ b/docs/Collie.html
@@ -1,5 +1,69 @@
-Collie
Idris2Doc : Collie
Collie
Collie: Command line interface for Idris2 applications
+
 
-Based on Guillaume Allais's agdARGS library:
+
+  
+  Collie
+  
+  
+
 
-https://github.com/gallais/agdargs/
(::) : (ParsedCommand (cmd .fst) (cmd .snd) -> a) -> Checkable (Handlers a) ((cmd .snd) .subcommands) -> Handlers a cmd
  Givent that we already have list syntax to build records, this gives us the
  ability to use list syntax to build `Handlers`: the head will be the handler
  for the toplevel command and the tail will go towards building the record of
  handlers for the subcommands.
  Totality: total
  Fixity Declaration: infixr operator, level 7
record Handlers : Type -> Field Command -> Type
  Totality: total
  Constructor: 
MkHandlers : (ParsedCommand (cmd .fst) (cmd .snd) -> a) -> Checkable (Handlers a) ((cmd .snd) .subcommands) -> Handlers a cmd

  Projections:
  
here : Handlers a cmd -> ParsedCommand (cmd .fst) (cmd .snd) -> a
  
there : Handlers a cmd -> Checkable (Handlers a) ((cmd .snd) .subcommands)
handle : ParseTree (cmd .snd) -> Handlers a cmd -> a
  Handling a parsetree is pretty simple: use `there` together with `(!!)` to
  select the appropriate subhandler while you're encountering the `There`
  constructor and finish up with `here`.
  Totality: total
(~~>) : Command arg -> Type -> Type
  A nicer notation for handlers
  Totality: total
  Fixity Declaration: infixr operator, level 4

\ No newline at end of file
+
+

+  Idris2Doc : Collie
+  
+
+  
+
+

+
Collie
Collie: Command line interface for Idris2 applications
+
+Based on Guillaume Allais's agdARGS library:
+
+https://github.com/gallais/agdargs/
+
Reexports
import public Collie.Core
import public Collie.Parser
import public Collie.Usage
import public Collie.Options.Domain
import public Collie.Options.Usual
import public Collie.Modifiers
import public Data.Record
import public Data.Record.SmartConstructors
import public Data.DPair
import public Data.Magma
import public Data.SnocList
import public System
Definitions
.parseArgs : (cmd : Command nm) -> HasIO io => io (Either String (ParseTreeT Maybe Maybe cmd))
  Totality: total
  Visibility: public export
record Handlers : Type -> Field Command -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkHandlers : (ParsedCommand (cmd .fst) (cmd .snd) -> a) -> Checkable (Handlers a) ((cmd .snd) .subcommands) -> Handlers a cmd

  Projections:
  
.here : Handlers a cmd -> ParsedCommand (cmd .fst) (cmd .snd) -> a
  
.there : Handlers a cmd -> Checkable (Handlers a) ((cmd .snd) .subcommands)
.here : Handlers a cmd -> ParsedCommand (cmd .fst) (cmd .snd) -> a
  Totality: total
  Visibility: public export
here : Handlers a cmd -> ParsedCommand (cmd .fst) (cmd .snd) -> a
  Totality: total
  Visibility: public export
.there : Handlers a cmd -> Checkable (Handlers a) ((cmd .snd) .subcommands)
  Totality: total
  Visibility: public export
there : Handlers a cmd -> Checkable (Handlers a) ((cmd .snd) .subcommands)
  Totality: total
  Visibility: public export
(::) : (ParsedCommand (cmd .fst) (cmd .snd) -> a) -> Checkable (Handlers a) ((cmd .snd) .subcommands) -> Handlers a cmd
  Givent that we already have list syntax to build records, this gives us the
  ability to use list syntax to build `Handlers`: the head will be the handler
  for the toplevel command and the tail will go towards building the record of
  handlers for the subcommands.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7
0 (~~>) : Command arg -> Type -> Type
  A nicer notation for handlers

  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 4
handle : ParseTree (cmd .snd) -> Handlers a cmd -> a
  Handling a parsetree is pretty simple: use `there` together with `(!!)` to
  select the appropriate subhandler while you're encountering  the `There`
  constructor and finish up with `here`.

  Totality: total
  Visibility: public export
.handleWith : (cmd : Command nm) -> cmd ~~> IO a -> IO a
  Finally we can put the various pieces together to get a toplevel command
  parsing the arguments and handling the resulting command using the
  user-provided handlers

  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Data.List.Fresh.Elem.html b/docs/Data.List.Fresh.Elem.html
index 607d7ff..6346398 100644
--- a/docs/Data.List.Fresh.Elem.html
+++ b/docs/Data.List.Fresh.Elem.html
@@ -1 +1,64 @@
-Data.List.Fresh.Elem
Idris2Doc : Data.List.Fresh.Elem
Data.List.Fresh.Elem
data Elem : a -> FreshList a neq -> Type
  Totality: total
  Constructors:
  
Here : Elem x x :: xs
  
There : Elem y xs -> Elem y x :: xs
recallId : (xs : FreshList a neq) -> (pos : Elem x xs) -> xs .recall pos = x
  Totality: total

\ No newline at end of file
+
+
+
+  
+  Data.List.Fresh.Elem
+  
+  
+
+
+
+

+  Idris2Doc : Data.List.Fresh.Elem
+  
+
+  
+
+

+
Data.List.Fresh.Elem
Definitions
data Elem : a -> FreshList a neq -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Here : Elem x (x :: xs)
  
There : Elem y xs -> Elem y (x :: xs)

  Hints:
  
Uninhabited (Here = There e)
  
Uninhabited (There e = Here)
.recall : (xs : FreshList a neq) -> Elem x xs -> a
  Totality: total
  Visibility: public export
recallId : (xs : FreshList a neq) -> (pos : Elem x xs) -> xs .recall pos = x
  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Data.List.Fresh.Quantifiers.SmartConstructors.html b/docs/Data.List.Fresh.Quantifiers.SmartConstructors.html
index a26c10e..f901c4e 100644
--- a/docs/Data.List.Fresh.Quantifiers.SmartConstructors.html
+++ b/docs/Data.List.Fresh.Quantifiers.SmartConstructors.html
@@ -1 +1,64 @@
-Data.List.Fresh.Quantifiers.SmartConstructors
Idris2Doc : Data.List.Fresh.Quantifiers.SmartConstructors
Data.List.Fresh.Quantifiers.SmartConstructors
(::) : {auto conArg : DecEq a} -> (xpx : DPair a (\x => p x)) -> {auto 0 pos : IsYes (isElem (xpx .fst) xs)} -> All p (remove (toWitness pos)) -> All p xs
  Totality: total
  Fixity Declaration: infixr operator, level 7
mkAny : {auto conArg : DecEq a} -> (x : a) -> {auto 0 _ : IsYes (isElem x xs)} -> p x -> Any p xs
  Totality: total

\ No newline at end of file
+
+
+
+  
+  Data.List.Fresh.Quantifiers.SmartConstructors
+  
+  
+
+
+
+

+  Idris2Doc : Data.List.Fresh.Quantifiers.SmartConstructors
+  
+
+  
+
+

+
Data.List.Fresh.Quantifiers.SmartConstructors
Definitions
mkAny : {auto {conArg:3089} : DecEq a} -> (x : a) -> {auto 0 _ : IsYes (isElem x xs)} -> p x -> Any p xs
  Totality: total
  Visibility: public export
(::) : {auto {conArg:3180} : DecEq a} -> (xpx : (x : a ** p x)) -> {auto 0 pos : IsYes (isElem (xpx .fst) xs)} -> All p (remove (toWitness pos)) -> All p xs
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7

\ No newline at end of file
diff --git a/docs/Data.List.Fresh.Quantifiers.html b/docs/Data.List.Fresh.Quantifiers.html
index c7cd525..3479f02 100644
--- a/docs/Data.List.Fresh.Quantifiers.html
+++ b/docs/Data.List.Fresh.Quantifiers.html
@@ -1 +1,64 @@
-Data.List.Fresh.Quantifiers
Idris2Doc : Data.List.Fresh.Quantifiers
Data.List.Fresh.Quantifiers
(!!) : All p xs -> (pos : Any q xs) -> p (lookup pos)
  Totality: total
  Fixity Declaration: infixr operator, level 4
any : ((x : a) -> Dec (p x)) -> (xs : FreshList a neq) -> Dec (Any p xs)
  Totality: total
insertLookedup : (pos : Any q xs) -> p (lookup pos) -> All p (remove pos) -> All p xs
  Totality: total
insertWith : ((y : a) -> q y -> p y) -> (pos : Any q xs) -> All p (remove pos) -> All p xs
  Totality: total
isElem : DecEq a => (x : a) -> (xs : FreshList a neq) -> Dec (Any (\{arg:0} => x = arg) xs)
  Totality: total
lookup : Any p xs -> a
  Totality: total
lookupWithProof : Any p xs -> DPair a (\x => p x)
  Totality: total
remove : Any p xs -> FreshList a neq
  Totality: total
sequence : Applicative f => All (f . p) xs -> f (All p xs)
  Totality: total
tabulate : ((x : a) -> p x) -> All p xs
  Totality: total
traverse : Applicative f => ((x : a) -> p x -> f (q x)) -> All p xs -> f (All q xs)
  Totality: total

\ No newline at end of file
+
+
+
+  
+  Data.List.Fresh.Quantifiers
+  
+  
+
+
+
+

+  Idris2Doc : Data.List.Fresh.Quantifiers
+  
+
+  
+
+

+
Data.List.Fresh.Quantifiers
Definitions
data Any : (0 _ : (a -> Type)) -> FreshList a neq -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Here : {auto 0 fresh : x # xs} -> p x -> Any p (x :: xs)
  
There : {auto 0 fresh : x # xs} -> Any p xs -> Any p (x :: xs)

  Hint: 
Uninhabited (Any p [])
data All : (0 _ : (a -> Type)) -> FreshList a neq -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Nil : All p []
  
(::) : p x -> {auto 0 fresh : x # xs} -> All p xs -> All p (x :: xs)
lookupWithProof : Any p xs -> (x : a ** p x)
  Totality: total
  Visibility: public export
lookup : Any p xs -> a
  Totality: total
  Visibility: public export
remove : Any p xs -> FreshList a neq
  Totality: total
  Visibility: public export
(!!) : All p xs -> (pos : Any q xs) -> p (lookup pos)
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 4
.toFreshList : All p xs -> FreshList (x : a ** p x) (neq `on` .fst)
  Totality: total
  Visibility: public export
0 .toFreshListFreshness : (rec : All p xs) -> y # xs -> (y ** {_:3728}) # rec .toFreshList
  Totality: total
  Visibility: public export
traverse : Applicative f => ((x : a) -> p x -> f (q x)) -> All p xs -> f (All q xs)
  Totality: total
  Visibility: public export
sequence : Applicative f => All (f . p) xs -> f (All p xs)
  Totality: total
  Visibility: public export
any : ((x : a) -> Dec (p x)) -> (xs : FreshList a neq) -> Dec (Any p xs)
  Totality: total
  Visibility: public export
isElem : DecEq a => (x : a) -> (xs : FreshList a neq) -> Dec (Any (\{arg:0} => x = {arg:0}) xs)
  Totality: total
  Visibility: public export
.update : Applicative f => All p xs -> (pos : Any q xs) -> (p (lookup pos) -> f (p (lookup pos))) -> f (All p xs)
  Totality: total
  Visibility: public export
map : ((x : a) -> p x -> q x) -> Any p xs -> Any q xs
  Map a function

  Totality: total
  Visibility: public export
map : ((x : a) -> p x -> q x) -> All p xs -> All q xs
  Map a function

  Totality: total
  Visibility: public export
mapSupport : ((pos : Any f xs) -> q (lookup pos)) -> All f xs -> All q xs
  Map a function restricted to the support of the list

  Totality: total
  Visibility: public export
tabulate : ((x : a) -> p x) -> All p xs
  Totality: total
  Visibility: public export
foldl : (b -> a -> b) -> b -> All (const a) xs -> b
  Totality: total
  Visibility: public export
foldr : (a -> b -> b) -> b -> All (const a) xs -> b
  Totality: total
  Visibility: public export
insertWith : ((y : a) -> q y -> p y) -> (pos : Any q xs) -> All p (remove pos) -> All p xs
  Totality: total
  Visibility: public export
insertLookedup : (pos : Any q xs) -> p (lookup pos) -> All p (remove pos) -> All p xs
  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Data.List.Fresh.html b/docs/Data.List.Fresh.html
index dba7245..acc4c5c 100644
--- a/docs/Data.List.Fresh.html
+++ b/docs/Data.List.Fresh.html
@@ -1,11 +1,70 @@
-Data.List.Fresh
Idris2Doc : Data.List.Fresh
Data.List.Fresh
Fresh lists, a variant of Catarina Coquand's contexts in "A
-Formalised Proof of the Soundness and Completeness of a Simply
-Typed Lambda-Calculus with Explicit Substitutions"
+
+
+
+  
+  Data.List.Fresh
+  
+  
+
+
+
+

+  Idris2Doc : Data.List.Fresh
+  
+
+  
 
-Based directly on Agda's fresh lists:
-http://agda.github.io/agda-stdlib/Data.List.Fresh.htmlFresh lists, a variant of Catarina Coquand's contexts in "A
+

+
Data.List.Fresh
Fresh lists, a variant of Catarina Coquand's contexts in "A
 Formalised Proof of the Soundness and Completeness of a Simply
-Typed Lambda-Calculus with Explicit Substitutions"
+Typed Lambda-Calculus with Explicit Substitutions"
 
-Based directly on Agda's fresh lists:
-http://agda.github.io/agda-stdlib/Data.List.Fresh.html
(#) : a -> FreshList a neq -> Type
  Totality: total
  Fixity Declaration: infix operator, level 5
(##) : a -> FreshList a neq -> Bool
  Totality: total
  Fixity Declaration: infix operator, level 4
BRel : Type -> Type
  Totality: total
Fresh : SnocList a -> Type
  Totality: total
data FreshList : (a : Type) -> BRel a -> Type
  Totality: total
  Constructors:
  
Nil : FreshList a neq
  
(::) : (x : a) -> (xs : FreshList a neq) -> {auto 0 _ : x # xs} -> FreshList a neq
cast : (sx : SnocList a) -> {auto 0 _ : Fresh sx} -> FreshList a neq
  Totality: total
castAux : (sx : SnocList a) -> (xs : FreshList a neq) -> {auto 0 _ : FreshSnoc sx xs} -> FreshList a neq
  Totality: total
decideFreshness : (x : a) -> (ys : FreshList a neq) -> Dec (x # ys)
  Totality: total
drop : Nat -> FreshList a neq -> FreshList a neq
  Totality: total
dropWhile : (a -> Bool) -> FreshList a neq -> FreshList a neq
  Totality: total
dropWhileFreshness : (pred : (a -> Bool)) -> (xs : FreshList a neq) -> y # xs -> y # dropWhile pred xs
  Totality: total
filter : (a -> Bool) -> FreshList a neq -> FreshList a neq
  Totality: total
filterFreshness : (pred : (a -> Bool)) -> (xs : FreshList a neq) -> y # xs -> y # filter pred xs
  Totality: total
foldl : (b -> a -> b) -> b -> FreshList a neq -> b
  Totality: total
foldr : (a -> b -> b) -> b -> FreshList a neq -> b
  Totality: total
fromMaybe : Maybe a -> FreshList a neq
  Totality: total
head : (xs : FreshList a neq) -> NonEmpty xs => a
  Totality: total
headFreshness : (0 x : a) -> (ys : FreshList a neq) -> {auto isNonEmpty : NonEmpty ys} -> x # ys -> So (neq x head ys)
  Totality: total
length : FreshList a neq -> Nat
  Totality: total
map : {0 A : Type} -> {0 Aneq : BRel A} -> {0 B : Type} -> {0 Bneq : BRel B} -> (F : (A -> B)) -> ((x : A) -> (y : A) -> So (Aneq x y) -> So (Bneq (F x) (F y))) -> FreshList A Aneq -> FreshList B Bneq
  Totality: total
mapFreshness : {0 A : Type} -> {0 Aneq : BRel A} -> {0 B : Type} -> {0 Bneq : BRel B} -> (F : (A -> B)) -> (Injectivity : ((x : A) -> (y : A) -> So (Aneq x y) -> So (Bneq (F x) (F y)))) -> (ys : FreshList A Aneq) -> x # ys -> F x # map ys
  Totality: total
tail : (xs : FreshList a neq) -> NonEmpty xs => FreshList a neq
  Totality: total
tailFreshness : (0 x : a) -> (ys : FreshList a neq) -> {auto isNonEmpty : NonEmpty ys} -> x # ys -> x # tail ys
  Totality: total
take : Nat -> FreshList a neq -> FreshList a neq
  Totality: total
takeFreshness : (n : Nat) -> (xs : FreshList a neq) -> y # xs -> y # take n xs
  Totality: total
takeWhile : (a -> Bool) -> FreshList a neq -> FreshList a neq
  Totality: total
takeWhileFreshness : (pred : (a -> Bool)) -> (xs : FreshList a neq) -> y # xs -> y # takeWhile pred xs
  Totality: total
toFreshList1 : FreshList a neq -> Maybe (FreshList1 a neq)
  Totality: total
uncons : FreshList a neq -> Maybe (a, FreshList a neq)
  Totality: total
Produced by Idris 2 version 0.4.0-c86184575

\ No newline at end of file
+Based directly on Agda's fresh lists:
+http://agda.github.io/agda-stdlib/Data.List.Fresh.html
+
Reexports
import public Data.So
Definitions
BRel : Type -> Type
  Totality: total
  Visibility: public export
(##) : a -> FreshList a neq -> Bool
  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 4
(#) : a -> FreshList a neq -> Type
  Totality: total
  Visibility: public export
  Fixity Declarations:
  infix operator, level 4
infixr operator, level 5
data FreshList : (a : Type) -> BRel a -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Nil : FreshList a neq
  
(::) : (x : a) -> (xs : FreshList a neq) -> {auto 0 _ : x # xs} -> FreshList a neq
data FreshList1 : (a : Type) -> BRel a -> Type
  Totality: total
  Visibility: public export
  Constructor: 
(::) : (x : a) -> (xs : FreshList a neq) -> {auto 0 _ : x # xs} -> FreshList1 a neq
map : {0 A : Type} -> {0 Aneq : BRel A} -> {0 B : Type} -> {0 Bneq : BRel B} -> (F : (A -> B)) -> ((x : A) -> (y : A) -> So (Aneq x y) -> So (Bneq (F x) (F y))) -> FreshList A Aneq -> FreshList B Bneq
  Totality: total
  Visibility: public export
0 mapFreshness : {0 A : Type} -> {0 Aneq : BRel A} -> {0 B : Type} -> {0 Bneq : BRel B} -> (F : (A -> B)) -> (Injectivity : ((x : A) -> (y : A) -> So (Aneq x y) -> So (Bneq (F x) (F y)))) -> (ys : FreshList A Aneq) -> x # ys -> F x # map ys
  Totality: total
  Visibility: public export
data Empty : FreshList a neq -> Type
  Totality: total
  Visibility: public export
  Constructor: 
Nil : Empty []
data NonEmpty : FreshList a neq -> Type
  Totality: total
  Visibility: public export
  Constructor: 
IsNonEmpty : NonEmpty (x :: xs)
length : FreshList a neq -> Nat
  Totality: total
  Visibility: public export
fromMaybe : Maybe a -> FreshList a neq
  Totality: total
  Visibility: public export
uncons : FreshList a neq -> Maybe (a, FreshList a neq)
  Totality: total
  Visibility: public export
toFreshList1 : FreshList a neq -> Maybe (FreshList1 a neq)
  Totality: total
  Visibility: public export
head : (xs : FreshList a neq) -> NonEmpty xs => a
  Totality: total
  Visibility: public export
tail : (xs : FreshList a neq) -> NonEmpty xs => FreshList a neq
  Totality: total
  Visibility: public export
0 .freshness : (xs : FreshList a neq) -> {auto isNonEmpty : NonEmpty xs} -> head xs # tail xs
  Totality: total
  Visibility: public export
0 headFreshness : (0 x : a) -> (ys : FreshList a neq) -> {auto isNonEmpty : NonEmpty ys} -> x # ys -> So (neq x (head ys))
  Totality: total
  Visibility: public export
0 tailFreshness : (0 x : a) -> (ys : FreshList a neq) -> {auto isNonEmpty : NonEmpty ys} -> x # ys -> x # tail ys
  Totality: total
  Visibility: public export
take : Nat -> FreshList a neq -> FreshList a neq
  Totality: total
  Visibility: public export
0 takeFreshness : (n : Nat) -> (xs : FreshList a neq) -> y # xs -> y # take n xs
  Totality: total
  Visibility: public export
drop : Nat -> FreshList a neq -> FreshList a neq
  Totality: total
  Visibility: public export
takeWhile : (a -> Bool) -> FreshList a neq -> FreshList a neq
  Totality: total
  Visibility: public export
0 takeWhileFreshness : (pred : (a -> Bool)) -> (xs : FreshList a neq) -> y # xs -> y # takeWhile pred xs
  Totality: total
  Visibility: public export
dropWhile : (a -> Bool) -> FreshList a neq -> FreshList a neq
  Totality: total
  Visibility: public export
0 dropWhileFreshness : (pred : (a -> Bool)) -> (xs : FreshList a neq) -> y # xs -> y # dropWhile pred xs
  Totality: total
  Visibility: public export
filter : (a -> Bool) -> FreshList a neq -> FreshList a neq
  Totality: total
  Visibility: public export
0 filterFreshness : (pred : (a -> Bool)) -> (xs : FreshList a neq) -> y # xs -> y # filter pred xs
  Totality: total
  Visibility: public export
decideFreshness : (x : a) -> (ys : FreshList a neq) -> Dec (x # ys)
  Totality: total
  Visibility: public export
foldl : (b -> a -> b) -> b -> FreshList a neq -> b
  Totality: total
  Visibility: public export
foldr : (a -> b -> b) -> b -> FreshList a neq -> b
  Totality: total
  Visibility: public export
(##) : BRel String
  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 4
FreshSnoc : SnocList a -> FreshList a neq -> Type
  Totality: total
  Visibility: public export
castAux : (sx : SnocList a) -> (xs : FreshList a neq) -> {auto 0 _ : FreshSnoc sx xs} -> FreshList a neq
  Totality: total
  Visibility: public export
Fresh : SnocList a -> Type
  Totality: total
  Visibility: public export
cast : (sx : SnocList a) -> {auto 0 _ : Fresh sx} -> FreshList a neq
  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Data.Magma.html b/docs/Data.Magma.html
index 26b8c56..bfd0c2e 100644
--- a/docs/Data.Magma.html
+++ b/docs/Data.Magma.html
@@ -1 +1,64 @@
-Data.Magma
Idris2Doc : Data.Magma
Data.Magma
record RawMagma : Type
  Totality: total
  Constructor: 
MkRawMagma : (Carrier : Type) -> (Carrier -> Carrier -> Carrier) -> RawMagma

  Projections:
  
Carrier : RawMagma -> Type
  
Product : (rec : RawMagma) -> Carrier rec -> Carrier rec -> Carrier rec
openMagma : (magma : RawMagma) -> Semigroup (magma .Carrier)
  Totality: total

\ No newline at end of file
+
+
+
+  
+  Data.Magma
+  
+  
+
+
+
+

+  Idris2Doc : Data.Magma
+  
+
+  
+
+

+
Data.Magma
Definitions
record RawMagma : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkRawMagma : (Carrier : Type) -> (Carrier -> Carrier -> Carrier) -> RawMagma

  Projections:
  
.Carrier : RawMagma -> Type
  
.Product : ({rec:0} : RawMagma) -> Carrier {rec:0} -> Carrier {rec:0} -> Carrier {rec:0}
.Carrier : RawMagma -> Type
  Totality: total
  Visibility: public export
Carrier : RawMagma -> Type
  Totality: total
  Visibility: public export
.Product : ({rec:0} : RawMagma) -> Carrier {rec:0} -> Carrier {rec:0} -> Carrier {rec:0}
  Totality: total
  Visibility: public export
Product : ({rec:0} : RawMagma) -> Carrier {rec:0} -> Carrier {rec:0} -> Carrier {rec:0}
  Totality: total
  Visibility: public export
rawMagma : Type -> RawMagma
  Totality: total
  Visibility: public export
rawMagma : RawMagma
  Totality: total
  Visibility: public export
rawMagma : RawMagma
  Totality: total
  Visibility: public export
rawMagma : RawMagma -> RawMagma
  Totality: total
  Visibility: public export
openMagma : (magma : RawMagma) -> Semigroup (magma .Carrier)
  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Data.Record.SmartConstructors.html b/docs/Data.Record.SmartConstructors.html
index 095bc83..5228758 100644
--- a/docs/Data.Record.SmartConstructors.html
+++ b/docs/Data.Record.SmartConstructors.html
@@ -1,3 +1,67 @@
-Data.Record.SmartConstructors
Idris2Doc : Data.Record.SmartConstructors
Data.Record.SmartConstructors
Selectively ported from agdARGS's Data.Recrod.SmartConstructors
+
 
-Please port more if you want!
BasicRecord : (Type -> Type) -> Fields (const Type) -> Type
  A record where the notion of type for its fields is `Type` itself
  Totality: total
mkBasicRecord : BasicRecord f flds -> BasicRecord f flds
  This acts as a type annotation ensuring the list passed as an
  argument is a basic record.
  Totality: total

\ No newline at end of file
+
+  
+  Data.Record.SmartConstructors
+  
+  
+
+
+
+

+  Idris2Doc : Data.Record.SmartConstructors
+  
+
+  
+
+

+
Data.Record.SmartConstructors
Selectively ported from agdARGS's Data.Recrod.SmartConstructors
+
+Please port more if you want!
+
Definitions
record Checkable : (Field a -> Type) -> Fields a -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCheckable : Record f flds -> Checkable f flds

  Projection: 
.mkCheckable : Checkable f flds -> Record f flds
.mkCheckable : Checkable f flds -> Record f flds
  Totality: total
  Visibility: public export
mkCheckable : Checkable f flds -> Record f flds
  Totality: total
  Visibility: public export
record Entry : (a : (String -> Type)) -> (Field a -> Type) -> Fields a -> Type
  Totality: total
  Visibility: public export
  Constructor: 
(::=) : (name : String) -> {auto 0 pos : IsYes (isField name flds)} -> f (field (toWitness pos)) -> Entry a f flds

  Projections:
  
.name : Entry a f flds -> String
  
0 .pos : ({rec:0} : Entry a f flds) -> IsYes (isField (name {rec:0}) flds)
  
.value : ({rec:0} : Entry a f flds) -> f (field (toWitness (pos {rec:0})))
.name : Entry a f flds -> String
  Totality: total
  Visibility: public export
name : Entry a f flds -> String
  Totality: total
  Visibility: public export
0 .pos : ({rec:0} : Entry a f flds) -> IsYes (isField (name {rec:0}) flds)
  Totality: total
  Visibility: public export
0 pos : ({rec:0} : Entry a f flds) -> IsYes (isField (name {rec:0}) flds)
  Totality: total
  Visibility: public export
.value : ({rec:0} : Entry a f flds) -> f (field (toWitness (pos {rec:0})))
  Totality: total
  Visibility: public export
value : ({rec:0} : Entry a f flds) -> f (field (toWitness (pos {rec:0})))
  Totality: total
  Visibility: public export
Nil : Checkable f []
  Totality: total
  Visibility: public export
(::) : (entry : Entry a f flds) -> Checkable f (remove (toWitness (entry .pos))) -> Checkable f flds
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7
record Inferrable : (Field a -> Type) -> Fields a -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkInferrable : Record f flds -> Inferrable f flds

  Projection: 
.mkInferrable : Inferrable f flds -> Record f flds
.mkInferrable : Inferrable f flds -> Record f flds
  Totality: total
  Visibility: public export
mkInferrable : Inferrable f flds -> Record f flds
  Totality: total
  Visibility: public export
record Entry : (a : (String -> Type)) -> (Field a -> Type) -> Type
  Totality: total
  Visibility: public export
  Constructor: 
(::=) : (name : String) -> f (name ** type) -> Entry a f

  Projections:
  
.name : Entry a f -> String
  
.type : ({rec:0} : Entry a f) -> a (name {rec:0})
  
.value : ({rec:0} : Entry a f) -> f (name {rec:0} ** type {rec:0})
.name : Entry a f -> String
  Totality: total
  Visibility: public export
name : Entry a f -> String
  Totality: total
  Visibility: public export
.type : ({rec:0} : Entry a f) -> a (name {rec:0})
  Totality: total
  Visibility: public export
type : ({rec:0} : Entry a f) -> a (name {rec:0})
  Totality: total
  Visibility: public export
.value : ({rec:0} : Entry a f) -> f (name {rec:0} ** type {rec:0})
  Totality: total
  Visibility: public export
value : ({rec:0} : Entry a f) -> f (name {rec:0} ** type {rec:0})
  Totality: total
  Visibility: public export
Nil : Inferrable f []
  Totality: total
  Visibility: public export
(::) : (entry : Entry a f) -> Inferrable f flds -> {auto 0 fresh : (entry .name ** entry .type) # flds} -> Inferrable f ((entry .name ** entry .type) :: flds)
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7
BasicRecord : (Type -> Type) -> Fields (const Type) -> Type
  A record where the notion of type for its fields is `Type` itself

  Totality: total
  Visibility: public export
mkBasicRecord : BasicRecord f flds -> BasicRecord f flds
  This acts as a type annotation ensuring the list passed as an
  argument is a basic record.

  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Data.Record.html b/docs/Data.Record.html
index 252710b..e118350 100644
--- a/docs/Data.Record.html
+++ b/docs/Data.Record.html
@@ -1,3 +1,66 @@
-Data.Record
Idris2Doc : Data.Record
Data.Record
An ordered record is a record whose field names have to appear in
-a fixed order, but must otherwise be distinct.An ordered record is a record whose field names have to appear in
-a fixed order, but must otherwise be distinct.
ArgList : Type
  Totality: total
Field : (String -> Type) -> Type
  Totality: total
Fields : (String -> Type) -> Type
  Totality: total
IsField : String -> Fields a -> Type
  Totality: total
IsFieldIrrelevant : (p : IsField nm flds) -> (q : IsField nm flds) -> p = q
  Totality: total
IsFieldStale : IsField nm flds -> fst nmv = nm -> (0 _ : nmv # flds) -> Void
  Totality: total
PartialRecord : (Field a -> Type) -> Fields a -> Type
  Totality: total
record Record : {0 A : String -> Type} -> (0 _ : (Field A -> Type)) -> (0 _ : Fields A) -> Type
  Totality: total
  Constructor: 
MkRecord : {0 A : String -> Type} -> {0 F : Field A -> Type} -> {0 Flds : Fields A} -> All F Flds -> Record F Flds

  Projection: 
content : {0 A : String -> Type} -> {0 F : Field A -> Type} -> {0 Flds : Fields A} -> Record F Flds -> All F Flds
TypeFields : Record (const Type) flds -> Fields (const Type)
  Totality: total
field : Any p flds -> Field a
  Totality: total
foldl : (b -> a -> b) -> b -> Record (const a) flds -> b
  Totality: total
isField : (fldName : String) -> (flds : Fields a) -> Dec (IsField fldName flds)
  Totality: total
isYesBecause : (d : Dec p) -> p -> IsYes d
  Totality: total
map : ((nm : String) -> a nm -> b nm) -> Fields a -> Fields b
  Totality: total
sequence : Applicative g => Record (g . f) flds -> g (Record f flds)
  Totality: total
soNotToEq : So (not b) -> b = False
  Totality: total
stringEq : x = y -> x == y = True
  Totality: total
tabulate : (args : ArgList) -> ((arg : String) -> Any (\{arg:0} => arg = arg) args -> a arg) -> Fields a
  Totality: total
tabulateFreshness : {0 a : String -> Type} -> (args : ArgList) -> (f : ((arg : String) -> Any (\{arg:0} => arg = arg) args -> a arg)) -> y # args -> MkDPair y u # tabulate args f
  Totality: total
traverse : Applicative m => ((x : Field a) -> f x -> m (g x)) -> Record f flds -> m (Record g flds)
  Totality: total

\ No newline at end of file
+
+
+
+  
+  Data.Record
+  
+  
+
+
+
+

+  Idris2Doc : Data.Record
+  
+
+  
+
+

+
Data.Record
An ordered record is a record whose field names have to appear in
+a fixed order, but must otherwise be distinct.
+
Reexports
import public Data.List.Fresh
import public Data.List.Fresh.Quantifiers
import public Decidable.Decidable.Extra1
import public Decidable.Equality
Definitions
ArgList : Type
  Totality: total
  Visibility: public export
Field : (String -> Type) -> Type
  Totality: total
  Visibility: public export
Fields : (String -> Type) -> Type
  Totality: total
  Visibility: public export
record Record : {0 A : String -> Type} -> (0 _ : (Field A -> Type)) -> (0 _ : Fields A) -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkRecord : {0 A : String -> Type} -> {0 F : Field A -> Type} -> {0 Flds : Fields A} -> All F Flds -> Record F Flds

  Projection: 
.content : {0 A : String -> Type} -> {0 F : Field A -> Type} -> {0 Flds : Fields A} -> Record F Flds -> All F Flds
.content : {0 A : String -> Type} -> {0 F : Field A -> Type} -> {0 Flds : Fields A} -> Record F Flds -> All F Flds
  Totality: total
  Visibility: public export
content : {0 A : String -> Type} -> {0 F : Field A -> Type} -> {0 Flds : Fields A} -> Record F Flds -> All F Flds
  Totality: total
  Visibility: public export
map : ((x : Field a) -> f x -> g x) -> Record f flds -> Record g flds
  Totality: total
  Visibility: public export
IsField : String -> Fields a -> Type
  Totality: total
  Visibility: public export
isYesBecause : (d : Dec p) -> p -> IsYes d
  Totality: total
  Visibility: public export
soNotToEq : So (not b) -> b = False
  Totality: total
  Visibility: public export
stringEq : x = y -> x == y = True
  Totality: total
  Visibility: public export
IsFieldStale : IsField nm flds -> fst nmv = nm -> (0 _ : nmv # flds) -> Void
  Totality: total
  Visibility: public export
IsFieldIrrelevant : (p : IsField nm flds) -> (q : IsField nm flds) -> p = q
  Totality: total
  Visibility: public export
isField : (fldName : String) -> (flds : Fields a) -> Dec (IsField fldName flds)
  Totality: total
  Visibility: public export
field : Any p flds -> Field a
  Totality: total
  Visibility: public export
.project : Record f flds -> (name : String) -> {auto pos : IsYes (isField name flds)} -> f (field (toWitness pos))
  Totality: total
  Visibility: public export
tabulate : (args : ArgList) -> ((arg : String) -> Any (\{arg:0} => arg = {arg:0}) args -> a arg) -> Fields a
  Totality: total
  Visibility: public export
0 tabulateFreshness : {0 a : String -> Type} -> (args : ArgList) -> (f : ((arg : String) -> Any (\{arg:0} => arg = {arg:0}) args -> a arg)) -> y # args -> (y ** u) # tabulate args f
  Totality: total
  Visibility: public export
map : ((nm : String) -> a nm -> b nm) -> Fields a -> Fields b
  Totality: total
  Visibility: public export
foldl : (b -> a -> b) -> b -> Record (const a) flds -> b
  Totality: total
  Visibility: public export
TypeFields : Record (const Type) flds -> Fields (const Type)
  Totality: total
  Visibility: public export
PartialRecord : (Field a -> Type) -> Fields a -> Type
  Totality: total
  Visibility: public export
traverse : Applicative m => ((x : Field a) -> f x -> m (g x)) -> Record f flds -> m (Record g flds)
  Totality: total
  Visibility: public export
sequence : Applicative g => Record (g . f) flds -> g (Record f flds)
  Totality: total
  Visibility: public export

\ No newline at end of file
diff --git a/docs/Decidable.Decidable.Extra1.html b/docs/Decidable.Decidable.Extra1.html
index aa71b64..e4d044e 100644
--- a/docs/Decidable.Decidable.Extra1.html
+++ b/docs/Decidable.Decidable.Extra1.html
@@ -1 +1,64 @@
-Decidable.Decidable.Extra1
Idris2Doc : Decidable.Decidable.Extra1
Decidable.Decidable.Extra1
toWitness : (0 _ : IsYes prf) -> a
  

\ No newline at end of file
+
+
+
+  
+  Decidable.Decidable.Extra1
+  
+  
+
+
+
+

+  Idris2Doc : Decidable.Decidable.Extra1
+  
+
+  
+
+

+
Decidable.Decidable.Extra1
Reexports
import public Decidable.Decidable
Definitions
toWitness : (0 _ : IsYes prf) -> a
  Visibility: public export

\ No newline at end of file
diff --git a/index.html b/index.html
index 6391baa..7101b1e 100644
--- a/index.html
+++ b/index.html
@@ -1 +1,64 @@
-collie
Idris2Doc : collie
Package collie - Namespaces

\ No newline at end of file
+
+
+
+  
+  collie
+  
+  
+
+
+
+

+  Idris2Doc : collie
+  
+
+  
+
+

+
Package collie - Namespaces

\ No newline at end of file