Commit e17f9958 authored by Ralf Jung's avatar Ralf Jung

Don't use Let outside of a section

parent b82abff8
......@@ -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 (lHl'). 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.
......
......@@ -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.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment