forked from leanprover-community/plausible
-
Notifications
You must be signed in to change notification settings - Fork 3
Open
Description
We're seeing arguments like (hypComps : List (List (α × List (List v) × List v))) in DeriveSchedules.lean, which is going to be hard to refactor and quite error prone IMHO.
We probably want to refactor this into a record with more descriptive names, and possibly alias the List type as well depending on its use.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels