Stream: Beginner Questions

Topic: "Bad name" when defining a datatype

Mario Xerxes Castelán Castro (Nov 29 2025 at 23:57):

I am following the tutorial. When I put datatype my_nat = 0 | Suc nat in a theory file, I get Bad name: "my_nat.0".

Mario Xerxes Castelán Castro (Nov 30 2025 at 02:53):

I fixed it by using zeroinstead of 0
.

Last updated: Dec 28 2025 at 12:45 UTC