matt-noonan / gdp

Ghosts of Departed Proofs
BSD 3-Clause "New" or "Revised" License
60 stars 11 forks source link

Missing COMPLETE pragma for The #20

Open isovector opened 2 years ago

isovector commented 2 years ago

Using The results in a non-exhaustive pattern match:

sizedBounds :: SizedQuadTree r a -> SizedRegion r
sizedBounds (The qt) = coerce $ bounds qt
    Pattern match(es) are non-exhaustive
    In an equation for ‘sizedBounds’:
        Patterns not matched: SizedQuadTree (QuadTree _ _)
   |
59 | sizedBounds (The qt) = coerce $ bounds qt
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^