val add_wrap (#n: nat) (x y: natN n) : natN n
let add_wrap (#n:nat) (x:natN n) (y:natN n) : natN n = if x + y < n then x + y else x + y - n
val add_wrap (#n: nat) (x y: natN n) : natN n
let add_wrap (#n: nat) (x y: natN n) : natN n =
if x + y < n then x + y else x + y - n
Vale.Def.Types_s.fst.checked
Vale.Lib.Seqs_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Types_s.fst
Prims.nat Vale.Def.Words_s.natN Prims.op_LessThan Prims.op_Addition Prims.bool Prims.op_Subtraction
module Vale.Def.Types_s

open FStar.Mul
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open Vale.Def.Words.Seq_s
open FStar.Seq
open Vale.Lib.Seqs_s

unfold let nat8 = Vale.Def.Words_s.nat8
unfold let nat16 = Vale.Def.Words_s.nat16
unfold let nat32 = Vale.Def.Words_s.nat32
unfold let nat64 = Vale.Def.Words_s.nat64
val add_wrap (#n: nat) (x y: natN n) : natN n
x: Vale.Def.Words_s.natN n -> y: Vale.Def.Words_s.natN n -> Vale.Def.Words_s.natN n