mechvel
mechvel
Personally I do not know. Currently I use my home-made functions ``` delP : {xs : List A} → Any P xs → List A delP {_ ∷ xs} (here...
> You should find (and be able to prove ;-)) that this is extensionally equivalent to Any._─_ as previously suggested, > so it's not obvious to me that you gain...
Sorry, `index` can mean in stdlib something different from a number. It may be a proof ``(i : x ∈ xs)`` for membership to a list.
Let the team decide. Anyway, double reversing (if any) will be bad here. Because `deleteFirst` will be run by interpreter or in executable, and it is easy to avoid double...
Following jamesmckinna, I consider replacing my `delP` with ``Data.List.Relation.Unary.Any ._─_ `` : ``` _─_ : {P : Pred A p} → ∀ xs → Any P xs → List A...
I meant that `prime-2` is a function, and `Prime 2` is its type.
For example , consider ``` record GCD a b ... where ... -- a version of Nat..GCD GCD[a,b]→GCD[b,a] : (a b : Carrier ) → GCD a b → GCD...
> Please could you provide a list of places where you think we don't follow suggestions 1 and 3. I am not ready to search for this. Here are several...
I suggest to start the function names with a lower-case symbols, including implications between predicates. For example, ``nonTrivial⇒NonZero`` (`NonZero` is capitalized here because it is a name of a type...
Please, remain the general `_∣_` definition untouched. My library uses the general `_∣_` widely. Its definition has been changed once, respectively this required an effort of me to change much...