Skip to content

Commit

Permalink
Merge pull request #58 from coq-community/mc_1223
Browse files Browse the repository at this point in the history
  • Loading branch information
proux01 authored Jun 29, 2024
2 parents 91ff6b8 + 5be6c5a commit 027788b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion theories/initctree.v
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ Lemma ctree_add_dyck_leaf_of m n d :
Proof.
elim: n m d => [|n IHn] m /=; first by rewrite addn0 gen_dyck_all_close.
elim: m => [|m IHm] d; rewrite doubleS /=; first by rewrite addn0 IHn.
by rewrite IHm IHn doubleS addnA -addnE !addnS.
by rewrite IHm IHn doubleS addnA -?addnE !addnS. (* TODO: remove ?addnE when requiring Coq >= 8.21 *)
Qed.

Lemma ctree_leaf_table_size h : size (ctree_leaf_table h) = h.+1.
Expand Down

0 comments on commit 027788b

Please sign in to comment.