Add properties that characterize `Data.Tree.AVL.Indexed.delete`. - #2961

Merged

JacquesCarette merged 14 commits into

agda:masterfrom

mikedelorimier:delete-multi

Apr 1, 2026

Commits on Mar 4, 2026

Add properties that characterize `Data.Tree.AVL.Indexed.delete`.
mikedelorimier
committed
bcc0843

Commits on Mar 20, 2026

telescoped arguments in Singleton.agda
mikedelorimier
committed
c373a14

Commits on Mar 21, 2026

removed unused vars, merged cases using Any.toSum for JoinConstFuns.agda
mikedelorimier
committed
9b18ec0

Commits on Mar 23, 2026

addressed review comments on Join.agda
mikedelorimier
committed
ab21b21
addressed comments in Insert.agda
mikedelorimier
committed
37b71a2
addressed review comments for HeadTail.agda
mikedelorimier
committed
90c3c97
addressed review comments for Delete.agda
mikedelorimier
committed
ce22932
Moved Data.Tree.AVL.Indexed.Relation.Unary.Any.* into Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.*
mikedelorimier
committed
4312608
Simplified proofs by removing subterms that recapitulate the subject function.
mikedelorimier
committed
ef68726
Changed whitespace to align matches.
mikedelorimier
committed
99adf46
More alignment.
mikedelorimier
committed
dce3e46

Commits on Mar 25, 2026

addressed review comments to use var in let and moved implicits to variable block
mikedelorimier
committed
ab2885d

Commits on Mar 26, 2026

Recorded changes in CHANGELOG.md. Addressed review comments for AnyLookup.
mikedelorimier
committed
6cfe7eb

Commits on Mar 27, 2026

Apply suggestion from @jamesmckinna
jamesmckinna
authored
0f071e1