pub const MATH_NAT: &str = r#"-- Natural Numbers
-- The foundation of arithmetic in type theory
-- Define the natural number type
Inductive Nat := Zero : Nat | Succ : Nat -> Nat.
-- Define some numbers
Definition one : Nat := Succ Zero.
Definition two : Nat := Succ one.
Definition three : Nat := Succ two.
-- Check the types
Check Zero.
Check Succ.
Check one.
Check two.
-- Evaluate expressions
Eval three.
"#;