coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question on Typeclasses and universes

From: richard Dapoigny <richard.dapoigny AT univ-smb.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Question on Typeclasses and universes
Date: Thu, 23 Apr 2020 12:51:26 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=richard.dapoigny AT univ-smb.fr; spf=Pass smtp.mailfrom=richard.dapoigny AT univ-smb.fr; spf=None smtp.helo=postmaster AT smtpout01-ext3.partage.renater.fr

Dear Coq users,

Suppose that I have the following elementary hierarchy:

Universes sf1 sf0.
Constraint sf0 < sf1.
Suppose now that I define type classes in sf0:

Polymorphic Cumulative Class XXX : Type@{sf0} := {

x1 : ...

In universe Type@{sf1} I can manipulate terms of Type@{sf0} but is there a way to check meta-properties of type classes such as whether XXX contains some particular fields (e.g., x1)?

(* by meta-properties I mean the name of the fields, and how many fields are there *)

Thanks in advance,

Richard

--
Richard Dapoigny
Associate Professor - LISTIC Laboratory
University Savoie Mont-Blanc
5, chemin de Bellevue
Po. Box 80439
Annecy-le-Vieux 74940
FRANCE
https://www.listic.univ-smb.fr/en/presentation-en/members/lecturers/richard-dapoigny-en/

****** People who don't know history are condemned to repeat it. ******

[Coq-Club] Question on Typeclasses and universes, richard Dapoigny, 04/23/2020