Theorem corpus for Theoria.Library.Nat.
These proofs document the initial natural number declarations, primitive recursion, and addition computations that reduce by reflexivity.
Summary
Functions
Returns the unelaborated proof syntax for theorem nat_add_one_left.
Elaborates and checks theorem nat_add_one_left against the given environment.
Returns the unelaborated type syntax for theorem nat_add_one_left.
Returns the unelaborated proof syntax for theorem nat_add_one_zero.
Elaborates and checks theorem nat_add_one_zero against the given environment.
Returns the unelaborated type syntax for theorem nat_add_one_zero.
Returns the unelaborated proof syntax for theorem nat_add_two_left.
Elaborates and checks theorem nat_add_two_left against the given environment.
Returns the unelaborated type syntax for theorem nat_add_two_left.
Returns the unelaborated proof syntax for theorem nat_add_two_zero.
Elaborates and checks theorem nat_add_two_zero against the given environment.
Returns the unelaborated type syntax for theorem nat_add_two_zero.
Returns the unelaborated proof syntax for theorem nat_add_zero_left.
Elaborates and checks theorem nat_add_zero_left against the given environment.
Returns the unelaborated type syntax for theorem nat_add_zero_left.
Returns the unelaborated proof syntax for theorem succ_is_function.
Elaborates and checks theorem succ_is_function against the given environment.
Returns the unelaborated type syntax for theorem succ_is_function.
Returns the unelaborated proof syntax for theorem zero_is_nat.
Elaborates and checks theorem zero_is_nat against the given environment.
Returns the unelaborated type syntax for theorem zero_is_nat.
Functions
Returns the unelaborated proof syntax for theorem nat_add_one_left.
Elaborates and checks theorem nat_add_one_left against the given environment.
Returns the unelaborated type syntax for theorem nat_add_one_left.
Returns the unelaborated proof syntax for theorem nat_add_one_zero.
Elaborates and checks theorem nat_add_one_zero against the given environment.
Returns the unelaborated type syntax for theorem nat_add_one_zero.
Returns the unelaborated proof syntax for theorem nat_add_two_left.
Elaborates and checks theorem nat_add_two_left against the given environment.
Returns the unelaborated type syntax for theorem nat_add_two_left.
Returns the unelaborated proof syntax for theorem nat_add_two_zero.
Elaborates and checks theorem nat_add_two_zero against the given environment.
Returns the unelaborated type syntax for theorem nat_add_two_zero.
Returns the unelaborated proof syntax for theorem nat_add_zero_left.
Elaborates and checks theorem nat_add_zero_left against the given environment.
Returns the unelaborated type syntax for theorem nat_add_zero_left.
Returns the unelaborated proof syntax for theorem succ_is_function.
Elaborates and checks theorem succ_is_function against the given environment.
Returns the unelaborated type syntax for theorem succ_is_function.
Returns the unelaborated proof syntax for theorem zero_is_nat.
Elaborates and checks theorem zero_is_nat against the given environment.
Returns the unelaborated type syntax for theorem zero_is_nat.