Stream: Coq users

Topic: Register section variable as a type class

view this post on Zulip Li-yao (Sep 05 2022 at 12:11):

Is it possible to use a variable as a type class in a section?

Section S.
Context (Klass : Type -> Type) (Klass_nat : Klass nat).

(* ??? *)

Existing Instance Klass_nat.

view this post on Zulip Gaëtan Gilbert (Sep 05 2022 at 12:13):

you can do an indirection through a constant, ie

Section S.
Context (Klass : Type -> Type).

Definition Klass' := Klass.
Existing Class Klass'.

Context  (Klass_nat : Klass' nat).

Existing Instance Klass_nat. (* not actually needed as variables are always instances *)

otherwise no

Last updated: Sep 28 2023 at 10:01 UTC