[FUTURE] Downstream agda-stdlib changes (related to lemmas about lists)

IntersectMBO / formal-ledger-specifications

Formal specifications of the cardano ledger

Apache License 2.0

38 stars 13 forks source link

[FUTURE] Downstream agda-stdlib changes (related to lemmas about lists) #563

Open omelkonian opened 2 months ago

omelkonian commented 2 months ago

When https://github.com/agda/agda-stdlib/pull/2479 is merged, which port stdlib additions from this repo, the task is to update the stdlib dependency and remove all these lemmas/definitions about lists:

Data/List/Ext.agda
Data/List/Ext/Properties.agda
Data/List/Relation/Binary/Sublist/Ext.agda
Data/List/Relation/Unary/Unique/Propositional/Properties/WithK.agda