In environment G : symbol -> option Z opts : symbolic_options_computed_opt t : API.type expr : API.Expr t d : dag inputs : list (idx + list idx) runtime_inputs : list (Z + list Z) Hinputs : Forall2 (eval_idx_or_list_idx G d) inputs runtime_inputs rets : list (idx + list idx) d' : dag Hwf : API.Wf expr The term "inputs" has type "list (idx + list idx)" while it is expected to have type "list (N * (idx + list idx))".