Skip to content
Snippets Groups Projects

add basic list functionality with Z-based indexing

Open Ralf Jung requested to merge ralf/listZ into master

This starts the work on #108 by implementing insert and index for Z as well as lengthZ, takeZ, dropZ, and porting much of the associated theory.

I have not ported everything, e.g. the interactions with Forall3, subseteq, submseteq, filter, mask are missing. Also there are more operations that would need a Z-based version, such as lookup_total, alter, delete, inserts, find, imap, imap2, resize, rotate, rotate_take, sublist_lookup, sublist_alter. There are also some tactics that will not handle these new operations and so might need adjustments or Z-based tactics: solve_length, simplify_list_eq.

Still I think this is a useful start that can serve as a foundation for later extensions. :)

Blocked on !441 (merged).

Edited by Ralf Jung

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
Please register or sign in to reply
Loading