blob: 67c7cfa35bb528d5511ff5888038929e1ea723b2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Require Import Coq.PArith.BinPosDef.
Local Open Scope positive_scope.
(** Append two sequences *)
Fixpoint app (p q:positive) : positive :=
match q with
| q~0 => (app p q)~0
| q~1 => (app p q)~1
| 1 => p~1
end.
|