Skip to content

Commit 908ff65

Browse files
mortbergmortberg
authored
Revert "Definition of OrderedCommRing (#1246)"
This reverts commit dc8f69e.
1 parent dc8f69e commit 908ff65

File tree

4 files changed

+0
-201
lines changed

4 files changed

+0
-201
lines changed

‎Cubical/Algebra/OrderedCommRing.agda‎

Lines changed: 0 additions & 3 deletions
This file was deleted.

‎Cubical/Algebra/OrderedCommRing/Base.agda‎

Lines changed: 0 additions & 136 deletions
This file was deleted.

‎Cubical/Relation/Binary/Order/Pseudolattice.agda‎

Lines changed: 0 additions & 3 deletions
This file was deleted.

‎Cubical/Relation/Binary/Order/Pseudolattice/Base.agda‎

Lines changed: 0 additions & 59 deletions
This file was deleted.

0 commit comments

Comments
 (0)