Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Zwei verschiedene Arten von nat (nat literal und NAT)
Warum gibt es zwei verschiedene Arten von natürlichen Zahlen in MMT (einmal in MitM Foundations und einmal in Urhteories / primitive types / nat ). Sequences verwendet z.B. das nat aus Urtheories “a ^ (b : NAT)”.
Es gibt so viele NATs wie jemand gemeint hat sie implementieren zu müssen 
in dem fall sind sie aber gleich: das NAT in MitM foundations müsste (eben gerade um sequences zum funktionieren zu bringen) über ecken als das NAT in urtheories definiert sein