Make IsTrunc an inductive type #1721
Annotations
6 errors and 10 warnings
|
Build HoTT:
theories/Categories/Category/Univalent.v#L22
No product even after head-reduction.
|
|
Build HoTT:
theories/Metatheory/FunextVarieties.v#L47
Not an inductive goal with 1 constructor.
|
|
Build HoTT:
theories/PropResizing/Nat.v#L268
No product even after head-reduction.
|
|
Build HoTT:
theories/Homotopy/Join/Core.v#L752
Not an inductive goal with 1 constructor.
|
|
Build HoTT:
theories/Pointed/Loops.v#L400
No product even after head-reduction.
|
|
Build HoTT:
theories/Classes/interfaces/abstract_algebra.v#L414
No product even after head-reduction.
|
|
Build HoTT:
theories/Basics/Overture.v#L134
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L138
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L195
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L325
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L338
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L339
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L348
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L382
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L396
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
Build HoTT:
theories/Basics/Overture.v#L401
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
The logs for this run have expired and are no longer available.
Loading