src/Util/Pos.v


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.