started refactoring TwoOneCat, in a broken state #16
Annotations
1 error and 8 warnings
|
Run coq-community/docker-coq-action@v1:
theories/WildCat/TwoOneCat.v#L38
UNDEFINED EVARS:
?X301==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d |- IsGraph ((a $-> b) * (b $-> c) * (c $-> d))]
(parameter isgraph_A of Is1Natural) {?isgraph_A}
?X303==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d |- Is2Graph (a $-> d)] (parameter is2graph_B of Is1Natural) {?is2graph_B}
?X304==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d |- Is01Cat (a $-> d)] (parameter is01cat_B of Is1Natural) {?is01cat_B}
?X305==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d |- Is1Cat (a $-> d)] (parameter is1cat_B of Is1Natural) {?is1cat_B}
?X339==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d |-
Is0Functor
(fun pat : (a $-> b) * (b $-> c) * (c $-> d) =>
let x := pat in
let fst := fst x in
let h := snd x in
let fst0 := fst in
let f := Overture.fst fst0 in let g := snd fst0 in h $o g $o f)]
(parameter is0functor_F of Is1Natural) {?is0functor_F}
?X367==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d |-
Is0Functor
(fun pat : (a $-> b) * (b $-> c) * (c $-> d) =>
let x := pat in
let fst := fst x in
let h := snd x in
let fst0 := fst in
let f := Overture.fst fst0 in let g := snd fst0 in h $o (g $o f))]
(parameter is0functor_G of Is1Natural) {?is0functor_G}
?X452==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d pat y h {f} g |- Is01Cat A] (parameter Is01Cat of cat_comp) {?Is01Cat}
?X461==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d pat y h {f} g |- Is01Cat A] (parameter Is01Cat of cat_comp) {?Is01Cat0}
?X549==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d pat p h {f} g |- Is01Cat A] (parameter Is01Cat of cat_comp) {?Is01Cat1}
?X558==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d pat p h {f} g |- Is01Cat A] (parameter Is01Cat of cat_comp) {?Is01Cat2}
?X569==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d pat p h f g |- IsTruncatedBicat A] (parameter IsTruncatedBicat
of bicat_assoc) {?IsTruncatedBicat}
?X570==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d {pat} {p} {h} {f} {g} |- IsGraph A] (parameter H of
bicat_assoc) {?H}
?X597==[IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
is1cat_2cells is1functor_bicat_postcomp is1functor_bicat_precomp
bifunctor_coh_comp bicat_assoc_inv bicat_idl_inv bicat_idr_inv a b
c d {pat} {p} {h} {f} {g} |- Is2Graph A] (parameter Is2Graph0 of
bicat_assoc) {?Is2Graph0}
CONSTRAINTS:
[] [IsBicategory A H H0 Is2Graph0 Is3Graph0 is_truncated_bicat
|
|
Run coq-community/docker-coq-action@v1
Could not find a terminator for warning:
File "./theories/Basics/Notations.v", line 13, characters 0-47:
Warning: Set ... Append is not supported.
[set-append-deprecated,deprecated-since-9.1,deprecated,default]
|
|
Run coq-community/docker-coq-action@v1:
theories/Basics/Notations.v#L13
Set ... Append is not supported.
|
|
Run coq-community/docker-coq-action@v1
Could not find a terminator for warning:
File "./theories/Basics/Notations.v", line 13, characters 0-47:
Warning: Set ... Append is not supported.
[set-append-deprecated,deprecated-since-9.1,deprecated,default]
theories/Basics/Notations.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 80596 ko)
|
|
Run coq-community/docker-coq-action@v1:
theories/Basics/Notations.v#L13
Set ... Append is not supported.
|
|
Run coq-community/docker-coq-action@v1
Could not find a terminator for warning:
File "./theories/Basics/Settings.v", line 10, characters 0-54:
Warning:
Legacy loading plugin method has been removed from Rocq, and the `:` syntax is deprecated, and its first argument ignored; please remove "ltac_plugin:" from your Declare ML
[legacy-loading-removed,deprecated-since-9.0,deprecated,default]
|
|
Run coq-community/docker-coq-action@v1
Could not find a terminator for warning:
File "./theories/Basics/Settings.v", line 10, characters 0-54:
Warning: "coq-core" has been renamed to "rocq-runtime".
[coq-core-plugin,deprecated-since-9.0,deprecated,default]
|
|
Run coq-community/docker-coq-action@v1:
theories/Basics/Settings.v#L10
"coq-core" has been renamed to "rocq-runtime".
|
|
Run coq-community/docker-coq-action@v1
Could not find a terminator for warning:
File "./theories/Basics/Settings.v", line 12, characters 0-90:
Warning:
Legacy loading plugin method has been removed from Rocq, and the `:` syntax is deprecated, and its first argument ignored; please remove "number_string_notation_plugin:" from your Declare ML
[legacy-loading-removed,deprecated-since-9.0,deprecated,default]
|
Loading