Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
stdpp
Commits
01f94618
Commit
01f94618
authored
Nov 09, 2017
by
Johannes Kloos
Browse files
Remove redundant instances
parent
e9a80032
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/infinite.v
View file @
01f94618
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From
stdpp
Require
Import
pretty
fin_collections
relations
prelude
.
From
stdpp
Require
Import
pretty
fin_collections
relations
prelude
gmap
.
(** The class [Infinite] axiomatizes types with infinitely many elements
by giving an injection from the natural numbers into the type. It is mostly
...
...
@@ -95,10 +95,3 @@ Section Fresh.
as
[
m
[
_
[->
[
notinX
belowinX
]]]]
;
auto
.
Qed
.
End
Fresh
.
(** Derive fresh instances. *)
Section
StringFresh
.
Context
`
{
FinCollection
string
C
,
!
RelDecision
elem_of
}.
Global
Instance
string_fresh
:
Fresh
string
C
:
=
fresh_generic
.
Global
Instance
string_fresh_spec
:
FreshSpec
string
C
:
=
fresh_generic_spec
.
End
StringFresh
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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