The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Hmm, apparently I can't compile GroupTheory library. My Coq version is:

The Coq Proof Assistant, version 8.4pl2 (June 2013)
compiled on Jun 30 2013 12:15:13 with OCaml 4.00.1

and error message is:

File "./g1.v", line 257, characters 0-21:
Error:
Found no subterm matching "star a (exp (neg (S n1)) a)" in the current goal.
make: *** [g1.vo] Error 1

any ideas about that?

Thanks,

---
Ömer Sinan Ağacan
http://osa1.net


2014/1/14 Ömer Sinan Ağacan 
<omeragacan AT gmail.com>:
> Wow, thanks all for your answers. This amount of code should keep me
> busy for a while. I hope I can understand the Coq used in these
> implementations.
>
> ---
> Ömer Sinan Ağacan
> http://osa1.net
>
>
> 2014/1/14 Vladimir Voevodsky 
> <vladimir AT ias.edu>:
>>
>> On Jan 14, 2014, at 3:18 PM, Daniil Frumin wrote:
>>
>>> Hi,
>>>
>>> There are many examples of proof of the specific theorems/properties
>>> on the internet: everything from blogposts to Coq contributions that
>>> Harley has linked.
>>>
>>> However, there are also bigger projects, like Math Classes [1], which
>>> aim is to develop interfaces (based on Coq's typeclasses) for many
>>> algebraic gadgets.
>>>
>>> Recently, Vladimir Voevodsky has published his paper [2] on his work
>>> in the formalization of mathematics. I haven't read it yet, but I
>>> guess it deals with Univalence, HoTT and other things I am clueless
>>> about.
>>>
>>> I myself tried to formalize basic category theory [3] and I've got to
>>> say it is going slower than I want and it is harder than I initially
>>> anticipated.
>>>
>>> [1] http://math-classes.org
>>> [2] http://arxiv.org/abs/1401.0053
>>> [2] http://repos.covariant.me/browse?r=cat;a=tree
>>
>>
>> There is a conceptually correct formalization of the basics of basic 
>> category theory here:
>>
>> https://github.com/benediktahrens/rezk_completion
>>
>> with the accompanying paper here:
>>
>> http://arxiv.org/abs/1303.0584
>>
>>
>> Vladimir.
>>
>>