Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
C
coq-stdpp
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
David Swasey
coq-stdpp
Commits
649f7c76
Commit
649f7c76
authored
Jan 03, 2017
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Document list_remove and list_remove_list.
parent
4fd8d550
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
14 additions
and
12 deletions
+14
-12
theories/list.v
theories/list.v
+14
-12
No files found.
theories/list.v
View file @
649f7c76
...
@@ -285,18 +285,20 @@ Inductive contains {A} : relation (list A) :=
...
@@ -285,18 +285,20 @@ Inductive contains {A} : relation (list A) :=
Infix "`contains`" := contains (at level 70) : C_scope.
Infix "`contains`" := contains (at level 70) : C_scope.
Hint Extern 0 (_ `contains` _) => reflexivity.
Hint Extern 0 (_ `contains` _) => reflexivity.
Section contains_dec_help.
(** Removes [x] from the list [l]. The function returns a [Some] when the
Context `{EqDecision A}.
+removal succeeds and [None] when [x] is not in [l]. *)
Fixpoint list_remove (x : A) (l : list A) : option (list A) :=
Fixpoint list_remove `{EqDecision A} (x : A) (l : list A) : option (list A) :=
match l with
match l with
| [] => None
| [] => None
| y :: l => if decide (x = y) then Some l else (y ::) <$> list_remove x l
| y :: l => if decide (x = y) then Some l else (y ::) <$> list_remove x l
end.
end.
Fixpoint list_remove_list (k : list A) (l : list A) : option (list A) :=
match k with
(** Removes all elements in the list [k] from the list [l]. The function returns
| [] => Some l | x :: k => list_remove x l ≫= list_remove_list k
a [Some] when the removal succeeds and [None] some element of [k] is not in [l]. *)
end.
Fixpoint list_remove_list `{EqDecision A} (k : list A) (l : list A) : option (list A) :=
End contains_dec_help.
match k with
| [] => Some l | x :: k => list_remove x l ≫= list_remove_list k
end.
Inductive Forall3 {A B C} (P : A → B → C → Prop) :
Inductive Forall3 {A B C} (P : A → B → C → Prop) :
list A → list B → list C → Prop :=
list A → list B → list C → Prop :=
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment