HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.58k stars 142 forks source link

The coverage check, Native type U60 --bug #463

Closed NaoEhSavio closed 4 months ago

NaoEhSavio commented 1 year ago

The coverage in the file, using the native type U60, depending on where the general case is, present a divergence of results Example 01: General case last or middle

Char.is_whitespace (c: Char) : Bool
Char.is_whitespace   9 = Bool.true
Char.is_whitespace  10 = Bool.true
Char.is_whitespace  11 = Bool.true
Char.is_whitespace  12 = Bool.true
Char.is_whitespace  13 = Bool.true
Char.is_whitespace  32 = Bool.true
Char.is_whitespace 133 = Bool.true
Char.is_whitespace 160 = Bool.true
Char.is_whitespace   c = Bool.false

This message appears, as if more cases are missing

   WARN  This function does not cover all the possibilities!
      • Missing case : _ 
      ┌──[Char/is_whitespace.kind2:2:1]
      │
      │    #kdl_name = Char_whtspc
      │    Char.is_whitespace (c: Char) : Bool
      │    ┬─────────────────
      │    └Here!
      │    Char.is_whitespace   9 = Bool.true

Example 02: General case in first

Char.is_whitespace (c: Char) : Bool
Char.is_whitespace   c = Bool.false
Char.is_whitespace   9 = Bool.true
Char.is_whitespace  10 = Bool.true
Char.is_whitespace  11 = Bool.true
Char.is_whitespace  12 = Bool.true
Char.is_whitespace  13 = Bool.true
Char.is_whitespace  32 = Bool.true
Char.is_whitespace 133 = Bool.true
Char.is_whitespace 160 = Bool.true
CHECKED  All terms checked.

It works perfectly

algebraic-dev commented 1 year ago

Fixed