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
Marianna Rapoport
iris-coq
Commits
fc0b90e4
Commit
fc0b90e4
authored
Nov 17, 2016
by
Ralf Jung
Browse files
Don't use Let outside of a section
parent
97ddb1f1
Changes
2
Hide whitespace changes
Inline
Side-by-side
prelude/finite.v
View file @
fc0b90e4
...
...
@@ -294,12 +294,13 @@ Proof.
rewrite
app_length
,
fmap_length
.
auto
.
Qed
.
Let
list_enum
{
A
}
(
l
:
list
A
)
:
∀
n
,
list
{
l
:
list
A
|
length
l
=
n
}
:
=
Definition
list_enum
{
A
}
(
l
:
list
A
)
:
∀
n
,
list
{
l
:
list
A
|
length
l
=
n
}
:
=
fix
go
n
:
=
match
n
with
|
0
=>
[[]
↾
eq_refl
]
|
S
n
=>
foldr
(
λ
x
,
(
sig_map
(
x
::
)
(
λ
_
H
,
f_equal
S
H
)
<$>
(
go
n
)
++))
[]
l
end
.
Program
Instance
list_finite
`
{
Finite
A
}
n
:
Finite
{
l
|
length
l
=
n
}
:
=
{|
enum
:
=
list_enum
(
enum
A
)
n
|}.
Next
Obligation
.
...
...
@@ -325,6 +326,7 @@ Next Obligation.
eexists
(
l
↾
Hl'
).
split
.
by
apply
(
sig_eq_pi
_
).
done
.
-
rewrite
elem_of_app
.
eauto
.
Qed
.
Lemma
list_card
`
{
Finite
A
}
n
:
card
{
l
|
length
l
=
n
}
=
card
A
^
n
.
Proof
.
unfold
card
;
simpl
.
induction
n
as
[|
n
IH
]
;
simpl
;
auto
.
...
...
prelude/stringmap.v
View file @
fc0b90e4
...
...
@@ -11,6 +11,7 @@ Notation stringmap := (gmap string).
Notation
stringset
:
=
(
gset
string
).
(** * Generating fresh strings *)
Section
stringmap
.
Local
Open
Scope
N_scope
.
Let
R
{
A
}
(
s
:
string
)
(
m
:
stringmap
A
)
(
n1
n2
:
N
)
:
=
n2
<
n1
∧
is_Some
(
m
!!
(
s
+
:
+
pretty
(
n1
-
1
))).
...
...
@@ -59,3 +60,4 @@ Fixpoint fresh_strings_of_set
let
x
:
=
fresh_string_of_set
s
X
in
x
::
fresh_strings_of_set
s
n
({[
x
]}
∪
X
)
end
%
nat
.
End
stringmap
.
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