Define Bools in Nat?

[ksqsf]

datatype Bool {
  true: Bool
  false: Bool
}

datatype Nat {
  zero: Bool
  suc(pred: Nat): Bool
}

check! Nat.zero : Bool

Is this expected behavior?

[xieyuheng]

No, this is error that should be reported by the type checker.

The following definition should not be allowed:

datatype Nat {
  zero: Bool
  suc(pred: Nat): Bool
}

Thanks for this feedback!

I will fix this soon.

[xieyuheng]

@xieyuheng test bot replay from tg