Theorem corpus for Theoria.Library.Vec.
Summary
Functions
Returns the unelaborated proof syntax for theorem vec_cons_is_function.
Elaborates and checks theorem vec_cons_is_function against the given environment.
Returns the unelaborated type syntax for theorem vec_cons_is_function.
Returns the unelaborated proof syntax for theorem vec_ind_cons_nat.
Elaborates and checks theorem vec_ind_cons_nat against the given environment.
Returns the unelaborated type syntax for theorem vec_ind_cons_nat.
Returns the unelaborated proof syntax for theorem vec_ind_nil_nat.
Elaborates and checks theorem vec_ind_nil_nat against the given environment.
Returns the unelaborated type syntax for theorem vec_ind_nil_nat.
Returns the unelaborated proof syntax for theorem vec_nil_is_vec.
Elaborates and checks theorem vec_nil_is_vec against the given environment.
Returns the unelaborated type syntax for theorem vec_nil_is_vec.
Functions
Returns the unelaborated proof syntax for theorem vec_cons_is_function.
Elaborates and checks theorem vec_cons_is_function against the given environment.
Returns the unelaborated type syntax for theorem vec_cons_is_function.
Returns the unelaborated proof syntax for theorem vec_ind_cons_nat.
Elaborates and checks theorem vec_ind_cons_nat against the given environment.
Returns the unelaborated type syntax for theorem vec_ind_cons_nat.
Returns the unelaborated proof syntax for theorem vec_ind_nil_nat.
Elaborates and checks theorem vec_ind_nil_nat against the given environment.
Returns the unelaborated type syntax for theorem vec_ind_nil_nat.
Returns the unelaborated proof syntax for theorem vec_nil_is_vec.
Elaborates and checks theorem vec_nil_is_vec against the given environment.
Returns the unelaborated type syntax for theorem vec_nil_is_vec.