G. Allais
G. Allais
Conor's disembodied voice tells me we should use a non-symmetric infix symbol for this non-symmetric action.
Yes please: if it grows enough, let's split it up according to the hierarchy!
You don't get irrelevant projections so IME it's nicer to package up things affected by the irrelevant modality so that you can project them out and pass them around to...
> like all non-checked documentation If we're going to do that then that documentation should 100% be generated by the CI using a simple Haskell program collecting such symbols and...
`with` gets stuck until you abstract over & match on the expression it mentions. A function with an `if_then_else_`-based RHS will unfold just fine, potentially making the goal noisier. I...
Be aware that it may take a while! Next week is the TYPES conference The week after that is the CALCO/MFPS joint conferences We may be able to meet after...
We're meeting tomorrow for a first go at this PR.
That last one is ongoing changes that are not thematically linked beyond being part of the review as a whole. We reset the commit before each new session, moving pure...
The new academic year is about to start so unfortunately I don't think I'll be able to come back to this for a while.
Catastrophic failure: ```idris import Data.List import Data.List.Elem import Decidable.Decidable import Decidable.Equality %default total toWitness : {prf1 : Dec a} -> IsYes prf1 -> a toWitness {prf1 = Yes prf2} x...