@Yann Leray
Require Import MSets.
Set Printing Universes.
Universe u.
Module T.
Declare Module X:TypElt.
Include MSetInterface.HasWOps X.
Goal Type@{u} = Type@{u}.
let t := type of fold in
match t with
forall _:?t, _ => exact (eq_refl t)
end.
Defined.
End T.
Print Universes.
Note that there is a #CUDW 2024 stream.
Last updated: Oct 13 2024 at 01:02 UTC