Jared Roesch
Jared Roesch
The other option is to use a signifying character like they do in Coq. ```coq Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y)....
It seems that we could get away with the ML type variable approach, just put a sigil in front like `'a` in order to signify that it is a type...
We recently met with a UW undergrad who was interested in implementing a SearchAbout/Hoogle/etc style feature for doing pattern & type based search. I'll check in with him this week...
@leodemoura I really like the idea of providing messages as "mini-documents', containing both human readable content as well as program fragments. It seems like a good way to experiment with...
While discussion continues I am asking that we hold off on voting so that all active contributors have a chance weigh in and comment. I know of at least two...
I am considering doing this as something I'm trying to support at work, is anyone else actively working on this? I was planning on building a new derive which will...