Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
how do i do this in isabelle?
(* how do i do this?? *)
function simplex_count :: "int⇒int⇒int" where
"simplex_count 0 0 = 1" |
"simplex_count 0 1 = 0" |
"simplex_count 1 0 = 2" |
"simplex_count n k = (simplex_count (n-1) k + simplex_count n (k-1))"
sorry
lemma simplex_count_lemma:
assumes "n simplex S" fixes k assumes "0 ≤ k" and "k ≤ n"
shows "k d_face_count S = simplex_count n k"
sorry
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.