Skip to content

Commit

Permalink
[ docs ] Make the natural language linter happier
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Jul 25, 2024
1 parent 929230e commit 1a2c522
Show file tree
Hide file tree
Showing 3 changed files with 5 additions and 3 deletions.
2 changes: 1 addition & 1 deletion deptycheck.ipkg
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ license = "MPL-2.0"
sourcedir = "src"
builddir = ".build"

version = 0.0.240702
version = 0.0.240724

modules = Deriving.DepTyCheck
, Deriving.DepTyCheck.Gen
Expand Down
2 changes: 1 addition & 1 deletion docs/source/explanation/derivation/design/single-con.md
Original file line number Diff line number Diff line change
Expand Up @@ -298,7 +298,7 @@ genD_idx_generated @{data_Nat} @{data_String} fuel b = data_D_giv_b fuel b
-->

In this case, generation of non-recursive constructors `JJ` and `TL` is straightforward,
the only difference is that `b` is a function argument, not a result of subgeneration.
the only difference is that `b` is a function parameter, not a result of subgeneration.

Recursive cases are not so easy.
Surely, we can first generate value `b` using derived `data_Bool` generator (as we did before for `JJ` constructor)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,9 @@ thus inapplicable directly for dependent types.
Since, we focus on total generators for dependent types, we cannot rely on common hybrid approach.
Considering all said above, it is decided to go the hard way and to do derivation of generators directly,
using metaprogramming facility if Idris called *elaboration scripts*.
% TODO to add a link to Idris documentation as soon as elaboration scripts are documented.
<!--
TODO to add a link to Idris documentation as soon as elaboration scripts are documented.
-->

Thus, DepTyCheck's derivation mechanism is a fully compile-time metaprogram that analyses generated datatype and
produces generator's code which is checked for type correctness and totality right after.

0 comments on commit 1a2c522

Please sign in to comment.