val reveal_all_defs:squash all_defs
let reveal_all_defs : squash all_defs = reveal_defs ()
val reveal_all_defs:squash all_defs
let reveal_all_defs:squash all_defs =
reveal_defs ()
Vale.Math.Poly2.fst.checked
Vale.Math.Poly2.Defs_s.fst.checked Vale.Math.Poly2.Defs.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked
Vale.Math.Poly2.fst
Vale.Math.Poly2_s.reveal_defs
module Vale.Math.Poly2
open FStar.Mul
module D = Vale.Math.Poly2.Defs_s
module I = Vale.Math.Poly2.Defs
open FStar.Seq
unfold let max = FStar.Math.Lib.max

let all_defs =
  poly == D.poly /\
  (forall (p:poly).{:pattern (degree p)} degree p == D.degree (to_poly p)) /\
  zero == of_poly D.zero /\
  one == of_poly D.one /\
  (forall (n:nat).{:pattern (monomial n)} monomial n == of_poly (D.monomial n)) /\
  (forall (p:poly) (n:int).{:pattern (shift p n)} shift p n == of_poly (D.shift (to_poly p) n)) /\
  (forall (p:poly) (n:nat).{:pattern (reverse p n)} reverse p n == of_poly (D.reverse (to_poly p) n)) /\
  (forall (p:poly) (n:int).{:pattern (poly_index p n)} poly_index p n == D.poly_index (to_poly p) n) /\
  (forall (a b:poly).{:pattern (add a b)} add a b == of_poly (D.add (to_poly a) (to_poly b))) /\
  (forall (a b:poly).{:pattern (mul a b)} mul a b == of_poly (D.mul (to_poly a) (to_poly b))) /\
  (forall (a b:poly).{:pattern (div a b)} degree b >= 0 ==> div a b == of_poly (D.div (to_poly a) (to_poly b))) /\
  (forall (a b:poly).{:pattern (mod a b)} degree b >= 0 ==> mod a b == of_poly (D.mod (to_poly a) (to_poly b)))
val reveal_all_defs:squash all_defs
Prims.squash Vale.Math.Poly2.all_defs