Started working on displayed functor category #13
Annotations
1 error
|
Run coq-community/docker-coq-action@v1:
theories/WildCat/DisplayedFunctor.v#L18
Not an inductive definition.
Command exited with non-zero status 1
|
Loading