Nathan van Doorn
Nathan van Doorn
This is a WIP because: - [x] I want to implement Cocartesian also - [ ] I want to look into doing something with ObjectRestriction to make this work a...
I'm very close but I can't quite get this proof across the line. Help would be very welcome.
It's defined as: ```agda record IndexedProduct {i} (I : Set i) : Set (i ⊔ o ⊔ e ⊔ ℓ) where field P : I → Obj productOf : IndexedProductOf...
I'm trying to implement something using SDL timers, but I was getting a segfault whenever the timer first triggered. I've got this down to a fairly small failing example: ```haskell...
My code: ```elm > parser = Parser.succeed (,) |= Parser.int |. Parser.symbol "x" |= Parser.int > Parser.run parser "1x1" ``` Expected output: ```elm ( 1, 1 ) : ( Int,...
One possible solution for #1427 I add versions of min, max, and dist that use primitive operations so they compile to fast code (hopefully - I admit I haven't checked...
This is consistent with the other names in the module as well as `Data.Rational.Properties`
Currently, for each bundle defined in `Algebra.Bundles`, there is a corresponding raw bundle, consisting of the operations but without the laws. The same is not true for `Algebra.Module.Bundles`. Should they...
We should add `Function.Metric.Rational.IsMetric (λ p q → ∣ p - q ∣)` to `Data.Rational.Properties` and maybe to `Data.Rational.Unnormalised.Properties` too
We have one approach to fields in `Algebra.Apartness.{Structures,Bundles}`. Another, stricter, approach is what nlab calls a "discrete field". This is a commutative ring with the following properties: ```agda invertibleOrZero :...