Constant-time indexing of closed type family axioms
CoAxiom stores a list of
CoAxBranches in a
BranchList. But it would be useful to actually have a constant-time indexing into axioms. One code fragment when I really wanted to have this feature is in
-- Replace n-th element in the list. Assumes 0-based indexing. replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch] replace_br brs n br = take n brs ++ [br] ++ drop (n+1) brs
I believe this code could be rewritten in a much more efficient way using constant-time indexing.
The new data structure should most likely have a type that indicates whether the axiom is branched or not.