The binary32 operations as a 32-bit machine and the specifications use
them: the model's, each result taken as the word it is. A binary32 result
IS a word, so on words these are the model's values exactly; with them the
statements proved for every choice of operations hold for the model with
no side condition (Proof.LinearStepCorrectForEveryShape, WarpSumCorrect,
HMMATileCorrect).
304def modelF32WordOperations : (family Float32Operations) = (f32OperationsOnWords modelF32Operations)The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.