jamesmckinna
jamesmckinna
I previously posted this on the Agda Zulip, #**newcomers>`where` clauses governing irrefutable `with` clauses** , but no-one answered (well, Matthew did, but he wasn't familiar with nested `with`...), and the...
So the issue title is a huge mouthful (and the text of this issue; -- sorry!), but the issue falls into two parts: * (general) ergonomics of 'pseudo' constructors/introduction forms...
Additionally, - [x] some dependencies lightened (in favour of other lemmas from `Data.Nat.Properties`) - [x] made corresponding changes to `
Is this a bug in the semantics of `--irrelevant-projections`, or of pattern-matching? Consider the following MWE (derived from a slightly more involved example): ```agda {-# OPTIONS --cubical-compatible --safe #-} module...
I'd like to extend `pattern` syntax to admit RHS which are not themselves patterns, but compute to such: ```agda module ComputedPattern where open import Agda.Builtin.Bool -- The following are acceptable...
Recent work by * [Choudhury and Fiore](https://entics.episciences.org/10492/pdf), on the free commutative monoid in HoTT, and * [Kupke, Forsberg, and Watters](https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/papers/freshlists_aplas2023.pdf) on fresh lists has looked at lists-modulo-permutation, with a view...
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...
This is a largely cosmetic coda to #2066 : * Completes the `Properties` by adding structure and bundle (NB transitivity has horrible indexed inference mess) * Sorts out alignment, standardises...
This is a sequel to #2294 mopping up the refactoring of `Data.Integer.Divisibility.Signed` suggested there. NB. * `Data.Integer.Divisibility` is still a 'minimal' collection of properties based on the underlying `Data.Nat.Divisibility`, so...
Task list to address #2201 , itemised by *what* needs to change (with proposed changes), rather than *where* (too many imports to list!): - [ ] `*.Bundles` as `Bundles` -...