Conversation
…a.Fin.Inductive. WIP
- Implicit argument added to toN - Implicit arguments in toN-injective slightly changed - Argument changed from implicit to explicit in elim
…emove Fin.Inductive, Fin.Inductive.Base, Fin.Inductive.Properties
|
Very nice! Unless anyone has any objections I will merge. @aljungstrom Har du några åsikter? |
|
May I suggest a change? Concretely, on my machine the following example get stuck during typechecking: But typechecks instantly with the change I am suggesting. Please feel free to ignore my comment if this suggestion doesn’t fit well with the current scope of the PR, or if you prefer to leave it for future work. |
|
@croos90 @mortberg I hope I haven't stalled this PR with my suggestion, and I apologize if that's the case. |
|
I think it would be better to merge this now, but it seems like I've lost my merge rights... Will merge once I've got my rights back. You can make a PR with the changes you suggest once this is merged this is merged and I'll try to merge that one fast |
|
Sorry for the late reply. Looks very good to me. Thanks for fixing this! I agree with @LorenzoMolena 's comment too -- I want to remember also having redefined it like this on a private branch. |
|
Merged! Please make a small follow-up PR @LorenzoMolena and I'll merge it quickly |
* Resolve naming inconsistency between Iso and Category.isIso (agda#1274) s/leftInv/ret; s/rightInv/sec --------- Co-authored-by: Madeleine Sydney Ślaga <msyds@deertopia.net> * isIso name change fix (agda#1281) * Update fin (agda#1279) * Exchange Fin in Cubical.Data.Fin for the deifinition from Cubical.Data.Fin.Inductive. WIP * Fixed finj, predFin, inject<, flast, ¬Fin0 to work with new definition of Fin. * Minor changes * Fix sumFinGen * fix any? * Everything type checks now. Important changes: - Implicit argument added to toN - Implicit arguments in toN-injective slightly changed - Argument changed from implicit to explicit in elim * some formatting * change ¬Fin0 * remove comments * Add <ᵗ-asym * make properties type check * Remove dependencies on Cubical.Data.Fin.Inductive.Base * Things that work * Properties type check * more working files * factorEquiv * comment fix * LehmerCode type checks * SumFin.Base type checks * some cleanup and Axiom.Choice type checks not reliant on old Fin * Remove dependence on Fin.Inductive * Remove dependence on Fin.Inductive * Remove dependency on Fin.Infuctive * Remove dependency on Fin.Inductive * Remove dependencies on Fin.Inductive * type check * fix FinSet * _<ᵗ_ is well founded * type checks with new Fin * Everything builds * Move everything from Fin.Inductive.Properties to Fin.Properties and remove Fin.Inductive, Fin.Inductive.Base, Fin.Inductive.Properties * some cleanup * more cleanup * fix trailing whitespaces * files end with newline --------- Co-authored-by: croos <76143n@gmail.com> * fix defintions of `min` and `max`, add comment on limitations of `UsingEq` (agda#1270) * Change implementation of Inductive Order on Nat (agda#1283) * use boolean comparison in `Nat.Order.Inductive`, add non-strict and flipped inductive order, make faster instance search in `Fin.Literals` * fix typo * Place holder for paper (agda#1286) * placeholder * whitespae * Cellpaper2 (agda#1287) * placeholder * whitespae * form * fix imports: `Fin.Inductive.Base/Properties` → `Fin.Base/Properties` --------- Co-authored-by: Madeleine Sydney Ślaga <65362461+msyds@users.noreply.github.com> Co-authored-by: Madeleine Sydney Ślaga <msyds@deertopia.net> Co-authored-by: Max S. New <maxsnew@gmail.com> Co-authored-by: Caroline Roos <croos.math@gmail.com> Co-authored-by: croos <76143n@gmail.com> Co-authored-by: Axel Ljungström <49276137+aljungstrom@users.noreply.github.com>
4 participants
Merge Data.Fin and Data.Fin.Inductive as per issue #1264