File tree Expand file tree Collapse file tree 1 file changed +6
-0
lines changed Expand file tree Collapse file tree 1 file changed +6
-0
lines changed Original file line number Diff line number Diff line change @@ -146,6 +146,12 @@ automate most of this.
146
146
as ` Structures ` etc.
147
147
NB. Historical legacy means that these conventions have not always been observed!
148
148
149
+ * Special case of the above for ` *-Reasoning ` (sub-)modules: by analogy with
150
+ ` Relation.Binary.PropositionalEquality.≡-Reasoning ` , when importing qualified
151
+ the ` -Reasoning ` (sub-)module associated with a given (canonical) choice of
152
+ symbol (eg. ` ≲ ` for ` Preorder ` reasoning), use the qualified name
153
+ ` <symbol>-Reasoning ` , ie. ` ≲-Reasoning ` for the example given.
154
+
149
155
* When using only a few items (i.e. < 5) from a module, it is a good practice to
150
156
enumerate the items that will be used by declaring the import statement
151
157
with the directive ` using ` . This makes the dependencies clearer, e.g.
You can’t perform that action at this time.
0 commit comments