Pi_parameters.One_public_input
val check :
switches:bool L.repr list ->
outer:L.scalar L.repr list ->
inner:L.scalar L.repr list list ->
bool L.repr L.t
predicate (in circuit form) on all of PI of the inner proofs and outer PI. giving the argument [x_1;x_2];[y_1;y_2]
means that x_1 ; x_2 are resp. the fst and second PI of the first inner proof and y_1;y_2 the fst and snd PI of the snd inner proof
val outer_of_inner : Main_Pack.scalar list list -> Main_Pack.scalar list
create outer from inner PI; note that the existence of this function restricts the outer PI to be computable from the inner PI.