search

thery / grobner

A fornalisation of Grobner basis in ssreflect
10 stars 3 forks source link

Integration to mathcomp #1

Open CohenCyril opened 5 years ago

CohenCyril commented 5 years ago

Hi @thery how about integrating your development to mathcomp?

thery commented 5 years ago

:+1: but what about multinomial is it still in?

palmskog commented 2 years ago

@thery how about adding grobner.v to CoqEAL? This way, more people will be able to use it, since CoqEAL is part of the Coq Platform. CoqEAL already depends on Multinomials. Finally, the CoqEAL theory is already a form of incubator for results to add to regular MathComp.

thery commented 2 years ago

@palmskog Yep that was the plan a long time ago (beginning of the phD of Damien (Roughling)), I see if I can find some energy to properly do this

thery commented 1 year ago

@palmskog https://github.com/coq-community/coqeal/pull/70