Theorem corpus for Theoria.Library.List.
These proofs document polymorphic list constructors and the first length computation over the standard Nat-backed list environment.
Summary
Functions
Returns the unelaborated proof syntax for theorem list_append_cons_left.
Elaborates and checks theorem list_append_cons_left against the given environment.
Returns the unelaborated type syntax for theorem list_append_cons_left.
Returns the unelaborated proof syntax for theorem list_append_nil_left.
Elaborates and checks theorem list_append_nil_left against the given environment.
Returns the unelaborated type syntax for theorem list_append_nil_left.
Returns the unelaborated proof syntax for theorem list_cons_is_function.
Elaborates and checks theorem list_cons_is_function against the given environment.
Returns the unelaborated type syntax for theorem list_cons_is_function.
Returns the unelaborated proof syntax for theorem list_length_cons_nil.
Elaborates and checks theorem list_length_cons_nil against the given environment.
Returns the unelaborated type syntax for theorem list_length_cons_nil.
Returns the unelaborated proof syntax for theorem list_length_cons.
Elaborates and checks theorem list_length_cons against the given environment.
Returns the unelaborated type syntax for theorem list_length_cons.
Returns the unelaborated proof syntax for theorem list_length_nil.
Elaborates and checks theorem list_length_nil against the given environment.
Returns the unelaborated type syntax for theorem list_length_nil.
Returns the unelaborated proof syntax for theorem list_length_singleton.
Elaborates and checks theorem list_length_singleton against the given environment.
Returns the unelaborated type syntax for theorem list_length_singleton.
Returns the unelaborated proof syntax for theorem list_length_two.
Elaborates and checks theorem list_length_two against the given environment.
Returns the unelaborated type syntax for theorem list_length_two.
Returns the unelaborated proof syntax for theorem list_nil_is_list.
Elaborates and checks theorem list_nil_is_list against the given environment.
Returns the unelaborated type syntax for theorem list_nil_is_list.
Functions
Returns the unelaborated proof syntax for theorem list_append_cons_left.
Elaborates and checks theorem list_append_cons_left against the given environment.
Returns the unelaborated type syntax for theorem list_append_cons_left.
Returns the unelaborated proof syntax for theorem list_append_nil_left.
Elaborates and checks theorem list_append_nil_left against the given environment.
Returns the unelaborated type syntax for theorem list_append_nil_left.
Returns the unelaborated proof syntax for theorem list_cons_is_function.
Elaborates and checks theorem list_cons_is_function against the given environment.
Returns the unelaborated type syntax for theorem list_cons_is_function.
Returns the unelaborated proof syntax for theorem list_length_cons_nil.
Elaborates and checks theorem list_length_cons_nil against the given environment.
Returns the unelaborated type syntax for theorem list_length_cons_nil.
Returns the unelaborated proof syntax for theorem list_length_cons.
Elaborates and checks theorem list_length_cons against the given environment.
Returns the unelaborated type syntax for theorem list_length_cons.
Returns the unelaborated proof syntax for theorem list_length_nil.
Elaborates and checks theorem list_length_nil against the given environment.
Returns the unelaborated type syntax for theorem list_length_nil.
Returns the unelaborated proof syntax for theorem list_length_singleton.
Elaborates and checks theorem list_length_singleton against the given environment.
Returns the unelaborated type syntax for theorem list_length_singleton.
Returns the unelaborated proof syntax for theorem list_length_two.
Elaborates and checks theorem list_length_two against the given environment.
Returns the unelaborated type syntax for theorem list_length_two.
Returns the unelaborated proof syntax for theorem list_nil_is_list.
Elaborates and checks theorem list_nil_is_list against the given environment.
Returns the unelaborated type syntax for theorem list_nil_is_list.