val equal (vecs1:t) (vecs2:t) : prop0
let equal vecs1 vecs2 = feq vecs1 vecs2
val equal (vecs1:t) (vecs2:t) : prop0
let equal vecs1 vecs2 =
feq vecs1 vecs2
Vale.PPC64LE.Vecs.fst.checked
Vale.PPC64LE.Machine_s.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.FunctionalExtensionality.fsti.checked
Vale.PPC64LE.Vecs.fst
Vale.PPC64LE.Vecs.t FStar.FunctionalExtensionality.feq Vale.PPC64LE.Machine_s.vec Vale.PPC64LE.Machine_s.quad32 Vale.Def.Prop_s.prop0
module Vale.PPC64LE.Vecs
open Vale.PPC64LE.Machine_s
open FStar.FunctionalExtensionality
val equal (vecs1:t) (vecs2:t) : prop0
vecs1: Vale.PPC64LE.Vecs.t -> vecs2: Vale.PPC64LE.Vecs.t -> Vale.Def.Prop_s.prop0