does lean have int8s

Stream: new members

[Alok Singh (S1'17)]

trying to formalize my friends formalization in haskell of a transformer computation model (RASP). was wondering if there's an int8 type builtin or importable

[Mario Carneiro]

it has Int and UInt8

[Alok Singh (S1'17)]

Damn. I wanted int8s specifically. I guess I can do { n : Z // n < 128 and
n >=-128}.

[Alok Singh (S1'17)]

this code gets stuck at OfNat synthesis but I'm unsure how to define an instance ofnat for int8 since not all nats are valid int8s

def Int8 := {n:Int // -128 ≤ n ∧ n < 128 }
def Int8.min: Int8 := -128
def Int8.max: Int8 := 127