agda
Tidy up `README` imports #2280
Brings the qualified imports into line with the emerging style-guidelines in line with #2280 .
Exceptions:
-
README.Data.List.Relation.Binary.Equality(which leaves holes open, moreover!?) -
README.Data.List.Membership(not clear how best to rename the qualified import names) -
README.Text.Tabular
Re: @JacquesCarette 's comment about 'horizontal' vs. 'vertical' layout of Feijen-style reasoning...
Unfortunately, this is self-inflicted. Changing L to List as the qualified name made the lines really long, moreover for me at least, very hard to read. As an Algebra of Programming person, I'm used to the more generous/expensive 'vertical' style, not least because it permits attention to be focused/localised on the reasons for a rewrite in the one line, while also separating out the individual terms for similar consideration on their own line(s).
In a library module, I might not care, but in a README, given that it is affording documentary/tutorial description, I though the the extra space was not actually harmful, if anything an improvement. But YMMV... potato/aardappel ;-)
Suggestion: create a local alias L for List for the scope of those proofs?
Ach! That suggestion is tantamount to the original qualified importas L!?