fact: Definition check_aux (a:atom) (t:Typ.type) : bool := match a with | Acop o => Typ.eqb (typ_cop o) t | Auop o a => let (ta,t') := typ_uop o in Typ.eqb t' t && Typ.eqb (get_type a) ta | Abop o a1 a2 => let (ta,t') := typ_bop o in let (ta1,ta2) := ta in Typ.eqb t' t && Typ.eqb (get_type a1) ta1 && Typ.eqb (get_type a2) ta2 | Atop o a1 a2 a3 => let (ta, t') := typ_top o in let '(ta1, ta2, ta3) := ta in Typ.eqb t' t && Typ.eqb (get_type a1) ta1 && Typ.eqb (get_type a2) ta2 && Typ.eqb (get_type a3) ta3 | Anop o a => let (ta,t') := typ_nop o in (Typ.eqb t' t) && (List.forallb (fun t1 => Typ.eqb (get_type t1) ta) a) | Aapp f args => let (targs,tr) := v_type _ _ (t_func.[f]) in check_args args targs && Typ.eqb tr t end.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList