Skip to content

duplicated code #1603

@affeldt-aist

Description

@affeldt-aist

analysis/theories/measure.v

Lines 1703 to 1710 in 229a6e9

#[global] Hint Extern 0 (measurable_fun _ (fun=> _)) =>
solve [apply: measurable_cst] : core.
#[global] Hint Extern 0 (measurable_fun _ (cst _)) =>
solve [apply: measurable_cst] : core.
#[global] Hint Extern 0 (measurable_fun _ id) =>
solve [apply: measurable_id] : core.
Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}.
Arguments measurable_fun_bool {d1 T1 D f} b.

Metadata

Metadata

Assignees

No one assigned

    Labels

    renaming/refactoring 🔧This is about a renaming or refactoring in the library

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions