`CoInductive` -> `Variant` #1880

Open

Labels

renaming/refactoring 🔧

Milestone

opened

analysis/theories/derive.v

Line 79 in 85fa9f6

CoInductive differentiable_def (f : V -> W) (x : filter_on V)

maybe this definition predates the introduction of Variant

Metadata

Assignees

No one assigned

Labels

renaming/refactoring 🔧

Type

No type

Projects

No projects

Milestone

1.16.0

Relationships

None yet

Development

No branches or pull requests