Module CombinatorsSource

telescope env sigma ctx turns a context x1:A1;...;xn:An into a right-associated nested sigma-type of the right sort. It returns:

• the nested sigma-type T := {x1:A1 & ... {xn-1:An-1 & ... An} ... }
• the canonical tuple (existsT _ x1 ... (existsT _ xn-1 xn) ...) inhabiting the sigma-type in the given context
• an instantiation of the assumptions of ctx with values they have in the context x:T, that is x1:=projT1 x;...;xn-1:=projT1 ... (projT2 x);xn:=projT2 ... (projT2 x); note that let-ins in the original context are preserved Depending on the sorts of types, it uses either ex, sig or sigT, even if we always used sigT above as an example.

make_iterated_tuple env sigma ~default c encapsulates c (of inferred type C) and its free variables x1,...,xn into a right-associated nested tuple in a sigT-type. It returns:

• the nested type {x1:A1 & ... {xn:An & ... C} ... }
• the tuple (existsT _ x1 ... (existsT _ xn c) ...)
• an alternative tuple (existsT _ x1 ... (existsT _ xn default) ...); if default has not the right type, it fails.

make_selector env sigma ~pos ~special ~default c constructs a case-split on c (assumed of inductive type), with the pos-th branch returning special, and all the other branch returning default.