The Coq mailing list

[1337 777 <1337777.net AT gmail.com>]

We at 1337777.net are also searching for such programmer, maybe we could concur with some joint proposal ?

One more possible angle of view for this question :

Here is some profitable example of some new tree widget for ur/web :

https://github.com/1337777/upo/blob/master/editableTree.urp

.. which shows ridiculously extreme 'sub-composability', as contrasted/dual to 'modulo'/'quotient',

and the techniques of 'sub-composability', type hiding/inference, the implicit/hidden inferred/unified arguments, function hidden arguments overloading, canonical unified structures, coercions, mixfix notations, parametric functors/'modules', higher/homotopical types ... are common now (ssr Mathematical _Components_, dedukti-modulo), but the technique of 'modulo' (some '_meta_' coherence/language, contrast to 'modulo _higher_ identities') are not common yet,

and in fact some recent proof exists which shows that this question can be very obscure-a-la-docteur d'etat ...

On Sat, Jul 18, 2015 at 3:17 AM, 1337 777 <1337777.net AT gmail.com> wrote:

We at 1337777.net are also searching for such programmer, maybe we could concur with some joint proposal ?

One possible angle of view for this question :

Here is some profitable example of some new list widget for ur/web :

https://github.com/1337777/upo/blob/master/examples/listEdit2.urp

.. ur/web is the initial bridge for translating the old edition of mathematics instead as some hypertextual programming activity,

and the old wikipedia/git/ed with [branching for simultaneous editiong] is in fact old, maybe the new are towards xslt transforms with [linear-jumping-modulo for simultaneous editing],

 and the contrast of encyclopedia-style contra school/courses/timed-browsing-style is to be clarified,

and the obsession with coulds a-la- [ Clide of Martin Ring ITP2014 or HELM/MOWGLI of Unibo or edukera.com ] is maybe questionable, and the possibility of delivery of the computations directly to the clients computers a-la-ur/web is more profitable, this immediately signify that any such attempt shall start by identifying/delimiting some lightweight/minimal alternative to any theorem prover coq/dedukti/... (a-la- smltojs interface) or simple mathematics non-formalising writer ..!1?