The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

I'm wondering if there is a clean way to to make a module type that carries a universe. What I would ideally want to do is something like:

Module Type Uni.

  Universe U.

End Uni.

Module Option (U : Uni).

  Inductive option (T : Type@{U.U}) : Type :=

  | None

  | Some (_ : T).

End.

But the universe U is not accessible. My attempt, which I do not think actually works is something like this:

Module Type Uni.

  Universe U.

  Parameter type : Type@{U}.

End Uni.

Module Option (U : Uni).

  Definition U := ltac:(match type of U.type with | ?T => exact T end).

  Inductive option (t : U) : Type :=

  | None

  | Some (_ : T).

End Option.

As far as I can tell though, the universe [U] seems to be fixed, and does not vary between different instances of the module type.

Does anyone know of a way to achieve this?

Thanks.

--

gregory malecha