Ali Caglayan
Ali Caglayan
Even the definition of iterated loops is problematic, is there some sort of where statement I can generate an instance with an fixpoint? ``` Require Import Basics. Definition loops (A...
@mikeshulman If I haven't misunderstood, there [is a variant here](https://coq.inria.fr/refman/addendum/implicit-coercions.html#coq:cmd.coercion) which says you can declare a coercion like a definition, and it magically puts it in the right class. Which...
Do you mean like this? ``` (* A pointed map is a map with a proof that it preserves the point *) Record pMap' (A B : pType) := {...
@JasonGross But the definition of iter_loops requires it to be already pointed. The definition of iter_loops I gave doesn't actually work.
@JasonGross Do you mean package everything together and then project out of it? This is exactly what we are doing at the moment. iterated_loops is exactly the kind of situation...
@mikeshulman Yes, I agree that it probably isn't doing anything. I don't know much about coercions apart from what I have inferred. There isn't much documentation on them either (at...
@JasonGross That definition was the one we had before I wrote the homotopy group file. At the time I had much difficulty proving the inner unfold lemma ``` Lemma unfold_loops...
@mikeshulman Yes this seems to solve the problem. I will see if I can get it to work with the rest of the library today. As it seems like this...
@JasonGross I don't think we can get it to work without pType right?
Are you doing this with regular coq? I can't get it to work in the library.