Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
David Swasey
coq-stdpp
Commits
1dee15b3
Commit
1dee15b3
authored
Mar 15, 2017
by
Robbert Krebbers
Browse files
Remove my name from the copyright headers.
parent
07d81355
Changes
37
Hide whitespace changes
Inline
Side-by-side
theories/base.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects type class interfaces, notations, and general theorems
(** This file collects type class interfaces, notations, and general theorems
that are used throughout the whole development. Most importantly it contains
that are used throughout the whole development. Most importantly it contains
...
...
theories/bset.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements bsets as functions into Prop. *)
(** This file implements bsets as functions into Prop. *)
From
stdpp
Require
Export
prelude
.
From
stdpp
Require
Export
prelude
.
...
...
theories/coPset.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements the type [coPset] of efficient finite/cofinite sets
(** This files implements the type [coPset] of efficient finite/cofinite sets
of positive binary naturals [positive]. These sets are:
of positive binary naturals [positive]. These sets are:
...
...
theories/collections.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on collections. Most
(** This file collects definitions and theorems on collections. Most
importantly, it implements some tactics to automatically solve goals involving
importantly, it implements some tactics to automatically solve goals involving
...
...
theories/countable.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Export
list
.
From
stdpp
Require
Export
list
.
Set
Default
Proof
Using
"Type"
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/decidable.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects theorems, definitions, tactics, related to propositions
(** This file collects theorems, definitions, tactics, related to propositions
with a decidable equality. Such propositions are collected by the [Decision]
with a decidable equality. Such propositions are collected by the [Decision]
...
...
theories/fin.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the fin type
(** This file collects general purpose definitions and theorems on the fin type
(bounded naturals). It uses the definitions from the standard library, but
(bounded naturals). It uses the definitions from the standard library, but
...
...
theories/fin_collections.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on finite collections. Most
(** This file collects definitions and theorems on finite collections. Most
importantly, it implements a fold and size function and some useful induction
importantly, it implements a fold and size function and some useful induction
...
...
theories/fin_map_dom.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file provides an axiomatization of the domain function of finite
(** This file provides an axiomatization of the domain function of finite
maps. We provide such an axiomatization, instead of implementing the domain
maps. We provide such an axiomatization, instead of implementing the domain
...
...
theories/fin_maps.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* 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 associate data to keys. This file defines an interface for
finite maps and collects some theory on it. Most importantly, it proves useful
finite maps and collects some theory on it. Most importantly, it proves useful
...
...
theories/finite.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Export
countable
vector
.
From
stdpp
Require
Export
countable
vector
.
Set
Default
Proof
Using
"Type"
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/gmap.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite maps and finite sets with keys of any countable
(** 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. *)
type. The implementation is based on [Pmap]s, radix-2 search trees. *)
...
...
theories/gmultiset.v
View file @
1dee15b3
(* Copyright (c) 2012-201
6
,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-201
7
,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Import
gmap
.
From
stdpp
Require
Import
gmap
.
Set
Default
Proof
Using
"Type"
.
Set
Default
Proof
Using
"Type"
.
...
...
theories/hashset.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set using hash maps. Hash sets are represented
(** 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
using radix-2 search trees. Each hash bucket is thus indexed using an binary
...
...
theories/lexico.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files defines a lexicographic order on various common data structures
(** 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. *)
and proves that it is a partial order having a strong variant of trichotomy. *)
...
...
theories/list.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on lists that
(** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *)
are not in the Coq standard library. *)
...
...
theories/listset.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates
(** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *)
removed. This implementation forms a monad. *)
...
...
theories/listset_nodup.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite as unordered lists without duplicates.
(** This file implements finite as unordered lists without duplicates.
Although this implementation is slow, it is very useful as decidable equality
Although this implementation is slow, it is very useful as decidable equality
...
...
theories/mapset.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files gives an implementation of finite sets using finite maps with
(** This files gives an implementation of finite sets using finite maps with
elements of the unit type. Since maps enjoy extensional equality, the
elements of the unit type. Since maps enjoy extensional equality, the
...
...
theories/natmap.v
View file @
1dee15b3
(* Copyright (c) 2012-2017,
Robbert Krebb
ers. *)
(* Copyright (c) 2012-2017,
Coq-std++ develop
ers. *)
(* This file is distributed under the terms of the BSD license. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements a type [natmap A] of finite maps whose keys range
(** 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
over Coq's data type of unary natural numbers [nat]. The implementation equips
...
...
Prev
1
2
Next
Write
Preview
Supports
Markdown
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