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