1signature fcpLib =
2sig
3    include Abbrev
4
5    val index_type    : Arbnum.num -> hol_type
6    val index_to_num  : hol_type -> Arbnum.num
7
8    val INDEX_CONV    : conv
9    val DIMINDEX      : Arbnum.num -> thm
10    val FINITE        : Arbnum.num -> thm
11    val SIZE          : Arbnum.num -> thm
12    val FCP_ss        : simpLib.ssfrag
13
14    val inst_fcp_lengths : term -> term
15end
16