Skip to content

measure_function.isFinite override fintype.isFinite #1943

@CohenCyril

Description

@CohenCyril

HB.mixin Record isFinite d (T : semiRingOfSetsType d) (R : numDomainType)
(k : set T -> \bar R) := { fin_num_measure : fin_num_fun k }.

We must rename this mixin otherwise declaring a type finite in a environment with all_analysis loaded leads to an error.

Metadata

Metadata

Assignees

No one assigned

    Labels

    "bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions