coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thomas Burdick <tfb AT cadence.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Differential Geometry Module Proposal
- Date: Mon, 13 Aug 2018 06:40:59 +0000
- Accept-language: fr-FR, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tfb AT cadence.com; spf=Pass smtp.mailfrom=tfb AT cadence.com; spf=Pass smtp.helo=postmaster AT NAM02-BL2-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:7K2AEh81zdyFLP9uRHKM819IXTAuvvDOBiVQ1KB31e4cTK2v8tzYMVDF4r011RmVBduds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55zebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZisJyg61VoRKuuxNwzpXOYI2JMfpzZL/RcMkYSGdHQ81fVzZBAoS5b4YXEeQBPeFYr4znqFsVsBCzGBSsBPnyxT9JmnD23rAx3uM9EQHIxwMtBM4Bv27Jo9rrMqcdTf66wLPUwjXEavNbwDHw45XGfBAmpPGDR7NwcczJxEYzDQzKk0ufqYr5MDyLzOgCr2+b7+9mWOmyiGAnsxl8riWzysojkIXEiYAYxkrK+Ch62oo4JN21RFZmbdOnEJZcrT+WO5Z0T884XW1luCg3xqcGtJO/ZCQKxoooyh3DZ/GCdoWH+A7sW/yeLDp9hX9oebayiAy3/Ee6yuDxVsa53VNOoydFj9XMuHYA3AHJ5MedUPty5EKh1C6P1w/N7uFEJlg5m7LHJpAm3rI8iIMfvFnFECPogUn2i7SZeVs+9uiv9uTnfq7pppiBN49ylw7yKLwumta4AeQkLAcBQ3Sb+eW71L3l50H5R6hKjuEykqnet5DaJt4XqbK+Aw9Qyooj6hC/ACm60NkAgHULMF1IdAiIgoXrIV3DLvP1Ae2+jlmsiDtrwurJPrzlApXDNHjDl7LhcK5h605S0wU+1sxQ6IhJBb4fJvL8RlH+uMbEAR8+Ngy42/znB8ll1oMCRWKPBbeUP7/VsV+R/+4gP+2MZJIOtzvmMPgk5/vujWcjllMHfKmp24EXaHGiEfh8LUWZeymkvtBUW2wNp081SPHgoFyESz9aIXioFepo7TYiTYmiEI3rR4a3gbXH0j3tTbNMYWUTNlCLFH7zP6+ZQfsNYyHadtNvmBQPXLSsTYQskxqpsVmpmPJcMuPI93hA5trY399v6riLzEBgxXlPF82Yllq1YSRxl2IMSSUx2fkk80d0xlqF2qU+iPtdR4UKu6F5FzwiPJuZ9NRUTsjoU1uaLNyARFugSdjgCjY0HIpono0+Jn1lEtDntSjtmiqnB7hJyO6tLblsqOf2+yK0IMxwjXHbyKMmkl8qBNNVMnGrjbJ+8A6VAJPVl0KelOChcqFOhSM=
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
I'm not aware of any such modules in Coq, but I'd be very interested to hear of any progress you make here!
Bon courage! Thomas
De : <coq-club-request AT inria.fr> au nom de Larry Lee <llee454 AT gmail.com>
EXTERNAL MAIL Hi,
I'm looking for mathematical fields that currently do not have any contributed developments and noticed that none of the modules listed in the Coq Package Index appeared to cover differential geometry. I'd like to develop a module covering basic results, but I'd like to avoid duplicating existing work. Does anyone know of any Coq modules that cover Differential Geometry? If not, would anyone like to share any recommendations/requests concerning the new module?
Thanks, - Larry Lee |
- [Coq-Club] Differential Geometry Module Proposal, Larry Lee, 08/09/2018
- Re: [Coq-Club] Differential Geometry Module Proposal, Li-yao Xia, 08/09/2018
- Re: [Coq-Club] Differential Geometry Module Proposal, Thomas Burdick, 08/13/2018
Archive powered by MHonArc 2.6.18.