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
S
stdpp
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
46
Issues
46
List
Boards
Labels
Service Desk
Milestones
Merge Requests
1
Merge Requests
1
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Iris
stdpp
Commits
22a06f37
Commit
22a06f37
authored
Mar 13, 2020
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Remove copyright headers, update LICENCE file.
This follows
iris!387
This closes issue
#54
.
parent
8db97649
Changes
43
Hide whitespace changes
Inline
Side-by-side
Showing
43 changed files
with
9 additions
and
91 deletions
+9
-91
LICENSE
LICENSE
+9
-7
theories/base.v
theories/base.v
+0
-2
theories/binders.v
theories/binders.v
+0
-2
theories/boolset.v
theories/boolset.v
+0
-2
theories/coGset.v
theories/coGset.v
+0
-2
theories/coPset.v
theories/coPset.v
+0
-2
theories/countable.v
theories/countable.v
+0
-2
theories/decidable.v
theories/decidable.v
+0
-2
theories/fin.v
theories/fin.v
+0
-2
theories/fin_map_dom.v
theories/fin_map_dom.v
+0
-2
theories/fin_maps.v
theories/fin_maps.v
+0
-2
theories/fin_sets.v
theories/fin_sets.v
+0
-2
theories/finite.v
theories/finite.v
+0
-2
theories/functions.v
theories/functions.v
+0
-2
theories/gmap.v
theories/gmap.v
+0
-2
theories/gmultiset.v
theories/gmultiset.v
+0
-2
theories/hashset.v
theories/hashset.v
+0
-2
theories/hlist.v
theories/hlist.v
+0
-2
theories/infinite.v
theories/infinite.v
+0
-2
theories/lexico.v
theories/lexico.v
+0
-2
theories/list.v
theories/list.v
+0
-2
theories/listset.v
theories/listset.v
+0
-2
theories/listset_nodup.v
theories/listset_nodup.v
+0
-2
theories/mapset.v
theories/mapset.v
+0
-2
theories/natmap.v
theories/natmap.v
+0
-2
theories/nmap.v
theories/nmap.v
+0
-2
theories/numbers.v
theories/numbers.v
+0
-2
theories/option.v
theories/option.v
+0
-2
theories/orders.v
theories/orders.v
+0
-2
theories/pmap.v
theories/pmap.v
+0
-2
theories/prelude.v
theories/prelude.v
+0
-2
theories/pretty.v
theories/pretty.v
+0
-2
theories/proof_irrel.v
theories/proof_irrel.v
+0
-2
theories/propset.v
theories/propset.v
+0
-2
theories/relations.v
theories/relations.v
+0
-2
theories/sets.v
theories/sets.v
+0
-2
theories/sorting.v
theories/sorting.v
+0
-2
theories/streams.v
theories/streams.v
+0
-2
theories/stringmap.v
theories/stringmap.v
+0
-2
theories/strings.v
theories/strings.v
+0
-2
theories/tactics.v
theories/tactics.v
+0
-2
theories/vector.v
theories/vector.v
+0
-2
theories/zmap.v
theories/zmap.v
+0
-2
No files found.
LICENSE
View file @
22a06f37
All files in this development are distributed under the terms of the BSD
license, included below.
Copyright: std++ developers and contributors
------------------------------------------------------------------------------
BSD LICENCE
...
...
@@ -12,18 +14,18 @@ modification, are permitted provided that the following conditions are met:
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
* Neither the name of the
<organization> nor the
names of its contributors may be used to endorse or promote products
derived from this software
without specific prior written permission.
* Neither the name of the
copyright holder nor the names of its contributors
may be used to endorse or promote products derived from this software
without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL
<COPYRIGHT HOLDER> BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
DISCLAIMED. IN NO EVENT SHALL
THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON
ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON
ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
theories/base.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects type class interfaces, notations, and general theorems
that are used throughout the whole development. Most importantly it contains
abstract interfaces for ordered structures, sets, and various other data
...
...
theories/binders.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements a type [binder] with elements [BAnon] for the
anonymous binder, and [BNamed] for named binders. This type is isomorphic to
[option string], but we use a special type so that we can define [BNamed] as
...
...
theories/boolset.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements boolsets as functions into Prop. *)
From
stdpp
Require
Export
prelude
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/coGset.v
View file @
22a06f37
(* Copyright (c) 2020, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements the type [coGset A] of finite/cofinite sets
of elements of any countable type [A].
...
...
theories/coPset.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements the type [coPset] of efficient finite/cofinite sets
of positive binary naturals [positive]. These sets are:
...
...
theories/countable.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From
Coq
.
QArith
Require
Import
QArith_base
Qcanon
.
From
stdpp
Require
Export
list
numbers
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/decidable.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects theorems, definitions, tactics, related to propositions
with a decidable equality. Such propositions are collected by the [Decision]
type class. *)
...
...
theories/fin.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the fin type
(bounded naturals). It uses the definitions from the standard library, but
renames or changes their notations, so that it becomes more consistent with the
...
...
theories/fin_map_dom.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file provides an axiomatization of the domain function of finite
maps. We provide such an axiomatization, instead of implementing the domain
function in a generic way, to allow more efficient implementations. *)
...
...
theories/fin_maps.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** Finite maps associate data to keys. This file defines an interface for
finite maps and collects some theory on it. Most importantly, it proves useful
induction principles for finite maps and implements the tactic
...
...
theories/fin_sets.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on finite sets. Most
importantly, it implements a fold and size function and some useful induction
principles on finite sets . *)
...
...
theories/finite.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Export
countable
vector
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/functions.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Export
base
tactics
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/gmap.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite maps and finite sets with keys of any countable
type. The implementation is based on [Pmap]s, radix-2 search trees. *)
From
stdpp
Require
Export
countable
infinite
fin_maps
fin_map_dom
.
...
...
theories/gmultiset.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Import
gmap
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/hashset.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set using hash maps. Hash sets are represented
using radix-2 search trees. Each hash bucket is thus indexed using an binary
integer of type [Z], and contains an unordered list without duplicates. *)
...
...
theories/hlist.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Import
tactics
.
Set
Default
Proof
Using
"Type"
.
Local
Set
Universe
Polymorphism
.
...
...
theories/infinite.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Export
list
.
From
stdpp
Require
Import
relations
pretty
.
...
...
theories/lexico.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files defines a lexicographic order on various common data structures
and proves that it is a partial order having a strong variant of trichotomy. *)
From
stdpp
Require
Import
numbers
.
...
...
theories/list.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *)
From Coq Require Export Permutation.
...
...
theories/listset.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *)
From
stdpp
Require
Export
sets
list
.
...
...
theories/listset_nodup.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite as unordered lists without duplicates.
Although this implementation is slow, it is very useful as decidable equality
is the only constraint on the carrier set. *)
...
...
theories/mapset.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files gives an implementation of finite sets using finite maps with
elements of the unit type. Since maps enjoy extensional equality, the
constructed finite sets do so as well. *)
...
...
theories/natmap.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements a type [natmap A] of finite maps whose keys range
over Coq's data type of unary natural numbers [nat]. The implementation equips
a list with a proof of canonicity. *)
...
...
theories/nmap.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [N]. *)
From
stdpp
Require
Import
pmap
mapset
.
...
...
theories/numbers.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects some trivial facts on the Coq types [nat] and [N] for
natural numbers, and the type [Z] for integers. It also declares some useful
notations. *)
...
...
theories/option.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the option
data type that are not in the Coq standard library. *)
From
stdpp
Require
Export
tactics
.
...
...
theories/orders.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** Properties about arbitrary pre-, partial, and total orders. We do not use
the relation [⊆] because we often have multiple orders on the same structure *)
From
stdpp
Require
Export
tactics
.
...
...
theories/pmap.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements an efficient implementation of finite maps whose keys
range over Coq's data type of positive binary naturals [positive]. The
implementation is based on Xavier Leroy's implementation of radix-2 search
...
...
theories/prelude.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Export
base
tactics
...
...
theories/pretty.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Export
strings
.
From
stdpp
Require
Import
relations
numbers
.
From
Coq
Require
Import
Ascii
.
...
...
theories/proof_irrel.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *)
From
stdpp
Require
Export
base
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/propset.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *)
From
stdpp
Require
Export
sets
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/relations.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on abstract rewriting systems.
These are particularly useful as we define the operational semantics as a
small step semantics. *)
...
...
theories/sets.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on sets. Most
importantly, it implements some tactics to automatically solve goals involving
sets. *)
...
...
theories/sorting.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
standard library, but without using the module system. *)
From
Coq
Require
Export
Sorted
.
...
...
theories/streams.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Export
tactics
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/stringmap.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements an efficient implementation of finite maps whose keys
range over Coq's data type of strings [string]. The implementation uses radix-2
search trees (uncompressed Patricia trees) as implemented in the file [pmap]
...
...
theories/strings.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From
Coq
Require
Import
Ascii
.
From
Coq
Require
Export
String
.
From
stdpp
Require
Export
list
.
...
...
theories/tactics.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose tactics that are used throughout
the development. *)
From
Coq
Require
Import
Omega
.
...
...
theories/vector.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on vectors
(lists of fixed length). It uses the definitions from the standard library, but
renames or changes their notations, so that it becomes more consistent with the
...
...
theories/zmap.v
View file @
22a06f37
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [Z]. *)
From
stdpp
Require
Import
pmap
mapset
.
...
...
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