fact: Fixpoint nthExprTypeFloat {Tl DefaultT} n (l : evalExprTypeFloat_list Tl) (default : evalExprTypeFloat DefaultT) := match n with | O => match Tl return evalExprTypeFloat_list Tl -> evalExprTypeFloat (nth O Tl DefaultT) with | nil => fun l' => default | T :: Tl' => match T with | Integer => fun l' => Int32.norm (fst l') | BinFloat => fun l' => fst l' end end l | S n' => match Tl return evalExprTypeFloat_list Tl -> evalExprTypeFloat (nth (S n') Tl DefaultT) with | nil => fun l' => default | T :: Tl' => fun l' => nthExprTypeFloat n' (snd l') default end l end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)