Skip to content

Commit

Permalink
Classes/theory/naturals: add debugging info
Browse files Browse the repository at this point in the history
  • Loading branch information
@jdchristensen
jdchristensen committed Oct 10, 2023
1 parent 5069961 commit 86c5276
Showing 1 changed file with 11 additions and 1 deletion.
12 changes: 11 additions & 1 deletion theories/Classes/theory/naturals.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,17 @@ Section borrowed_from_nat.
pose (Q := fun s : SemiRings.Operations =>
forall P : s -> Type, P 0 -> (forall n, P n -> P (1 + n)) -> forall n, P n).
change (Q (SemiRings.BuildOperations N)).
apply (from_nat_stmt nat).

(* Material added while testing. *)
Set Printing Universes.
#[global] Typeclasses Transparent Lt.
assert (Zero@{U} nat).
1: exact _. (* This one works. *)
assert (Lt@{U U} nat).
Fail 1: exact _. (* Lt fails. "Could not find an instance ..." I didn't try the other seven. *)
1: apply nat_lt.

apply (from_nat_stmt nat). (** Error here, looking for nine typeclass instances. *)

Check failure on line 144 in theories/Classes/theory/naturals.v

View workflow job for this annotation

GitHub Actions / build (supported) 


Unable to satisfy the following constraints:
In environment:
H : Funext
H0 : Univalence
N : Type@{U}
Aap : Apart@{U U} N
Aplus : Plus@{U} N
Amult : Mult@{U} N
Azero : Zero@{U} N
Aone : One@{U} N
Ale : Le@{U U} N
Alt : Lt@{U U} N
U : NaturalsToSemiRing@{U U} N
H1 : Naturals@{U U U U U U U U} N
Q := fun s : Operations@{HoTT.Classes.theory.naturals.2049 U} =>
forall P : s -> Type@{HoTT.Classes.theory.naturals.2050},
P 0 -> (forall n : s, P n -> P (1 + n)) -> forall n : s, P n
: Operations@{HoTT.Classes.theory.naturals.2049 U} ->
Type@{HoTT.Classes.theory.naturals.2066}
X : Zero@{U} nat
X0 : Lt@{U U} nat

?Aap0 : "Apart@{U U} nat"

?Aplus0 : "Plus@{U} nat"

?Amult0 : "Mult@{U} nat"

?Azero0 : "Zero@{U} nat"

?Aone0 : "One@{U} nat"

?Ale0 : "Le@{U U} nat"

?Alt0 : "Lt@{U U} nat"

?U0 : "NaturalsToSemiRing@{U U} nat"

?H2 : "Naturals@{U U U U U U U U} nat"


Command exited with non-zero status 1

Check failure on line 144 in theories/Classes/theory/naturals.v

View workflow job for this annotation

GitHub Actions / build (latest) 


Unable to satisfy the following constraints:
In environment:
H : Funext
H0 : Univalence
N : Type@{U}
Aap : Apart@{U U} N
Aplus : Plus@{U} N
Amult : Mult@{U} N
Azero : Zero@{U} N
Aone : One@{U} N
Ale : Le@{U U} N
Alt : Lt@{U U} N
U : NaturalsToSemiRing@{U U} N
H1 : Naturals@{U U U U U U U U} N
Q := fun s : Operations@{HoTT.Classes.theory.naturals.2049 U} =>
forall P : s -> Type@{HoTT.Classes.theory.naturals.2050},
P 0 -> (forall n : s, P n -> P (1 + n)) -> forall n : s, P n
: Operations@{HoTT.Classes.theory.naturals.2049 U} ->
Type@{HoTT.Classes.theory.naturals.2066}
X : Zero@{U} nat
X0 : Lt@{U U} nat

?Aap0 : "Apart@{U U} nat"

?Aplus0 : "Plus@{U} nat"

?Amult0 : "Mult@{U} nat"

?Azero0 : "Zero@{U} nat"

?Aone0 : "One@{U} nat"

?Ale0 : "Le@{U U} nat"

?Alt0 : "Lt@{U U} nat"

?U0 : "NaturalsToSemiRing@{U U} nat"

?H2 : "Naturals@{U U U U U U U U} nat"


Command exited with non-zero status 1

Check failure on line 144 in theories/Classes/theory/naturals.v

View workflow job for this annotation

GitHub Actions / build (dev, --warnings) 


Unable to satisfy the following constraints:
In environment:
H : Funext
H0 : Univalence
N : Type@{U}
Aap : Apart@{U U} N
Aplus : Plus@{U} N
Amult : Mult@{U} N
Azero : Zero@{U} N
Aone : One@{U} N
Ale : Le@{U U} N
Alt : Lt@{U U} N
U : NaturalsToSemiRing@{U U} N
H1 : Naturals@{U U U U U U U U} N
Q := fun s : Operations@{HoTT.Classes.theory.naturals.2049 U} =>
forall P : s -> Type@{HoTT.Classes.theory.naturals.2050},
P 0 -> (forall n : s, P n -> P (1 + n)) -> forall n : s, P n
: Operations@{HoTT.Classes.theory.naturals.2049 U} ->
Type@{HoTT.Classes.theory.naturals.2066}
X : Zero@{U} nat
X0 : Lt@{U U} nat

?Aap0 : "Apart@{U U} nat"

?Aplus0 : "Plus@{U} nat"

?Amult0 : "Mult@{U} nat"

?Azero0 : "Zero@{U} nat"

?Aone0 : "One@{U} nat"

?Ale0 : "Le@{U U} nat"

?Alt0 : "Lt@{U U} nat"

?U0 : "NaturalsToSemiRing@{U U} nat"

?H2 : "Naturals@{U U U U U U U U} nat"


Command exited with non-zero status 1
unfold Q;clear Q.
simpl.
exact nat_induction.
Expand Down

0 comments on commit 86c5276

Please sign in to comment.