Document Vatras.Lang.All(.Fixed)

Author: ibbem

src/Vatras/Lang/All.agda

@@ -1,7 +1,13 @@
 {-|
 This module reexports all our language definitions as new modules.
-If you intend to work with more than one language in a file
-we recommend using this module to easily import the languages you need.
+Instead of directly importing the language modules,
+we recommend importing this module if you do not want to apply the module parameters.
+
+For convenience, we change explicit module parameters to implicit ones where useful.
+The rule of thumb is:
+  Types use explicit arguments whereas functions use implicit arguments.
+In case you want to instantiate these module parameters with a fixed value,
+you can use `Vatras.Lang.All.Fixed` instead of this module.
 -}
 module Vatras.Lang.All where
 
@@ -21,6 +27,12 @@ open import Size using (∞)
 open import Vatras.Framework.Definitions using (𝔽; 𝔸; 𝕍)
 open import Vatras.Framework.Variants using (Rose)
 
+{-
+Some definitions do not make use of the module parameter.
+In such cases explicit arguments would be confusing and implicit paramters would lead to unsolved metas.
+Hence, we assert that these parameters are unused by passing `⊥` for `𝔽` or `λ _ → ⊥` for `𝔸`.
+-}
+
 module VariantList where
   open Vatras.Lang.VariantList using (VariantList; VariantListL; Clone-and-Own) public
   open Vatras.Lang.VariantList (λ _ → ⊥) using (Configuration) public

src/Vatras/Lang/All/Fixed.agda

@@ -17,6 +17,7 @@ import Vatras.Lang.Gruler
 module VariantList = Vatras.Lang.VariantList V
 module CCC = Vatras.Lang.CCC F
 module NCC where
+  -- Similar as in `Vatras.Lang.All`, we make the arity argument implicit for usablity.
   open Vatras.Lang.NCC F using (NCC; NCCL; Configuration) public
   module _ {n : ℕ≥ 2} where
     open Vatras.Lang.NCC F n hiding (NCC; NCCL; Configuration) public