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