learn_record.v

Require Import
  Coq.FSets.FMapAVL
  Coq.FSets.FMapFacts
  Coq.Structures.OrderedTypeEx
  PeanoNat.

Module Import M := FMapAVL.Make(Nat_as_OT).
Print Module M.
Check (M.t (list nat)).

Lemma hello : M.t (list nat).
Proof.
exact (M.add 0 (cons 0 nil) (M.empty _)).
Qed.


Definition state := ( M.t (list nat) * M.t nat * M.t nat )%type.

Record StateSSS : Set := mkState
{
  u8_map : M.t (list nat) ;
}.

我想要一个包含 nat -> list nat 的 Record，但是编译不过

Universe inconsistency. Cannot enforce E.t.u0 <= Set.

另外，nat -> list nat 的map的写法通常是要用 FMapAVL 吗？