Instances of apartness structures for common numeric types #1733

Closed

Closed

Instances of apartness structures for common numeric types#1733

Labels

additionlow-hanging-fruit

ℚᵘ is a HeytingField Added Unnormalised Rational Field Structure #1959
ℚ is a HeytingField Decidable Setoid -> Apartness Relation and Rational Heyting Field #2194

Metadata

Assignees

No one assigned

Labels

additionlow-hanging-fruit

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests