Stream: Coq devs & plugin devs

Topic: cudw 2024


view this post on Zulip Gaëtan Gilbert (Jul 01 2024 at 12:11):

@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.

view this post on Zulip Théo Zimmermann (Jul 01 2024 at 12:56):

Note that there is a #CUDW 2024 stream.


Last updated: Oct 13 2024 at 01:02 UTC