fact: Fixpoint PlotLine (A : CR*CR -> Prop) (i:nat) (r step:Q) (y : CR) (d e:Q) (ltde : d < e) (loc : LocatedSubset (ProductMS CR CR) A) { struct i } : list bool := match i with | O => nil | S p => cons (let xi := inject_Q_CR (r - inject_Z (Z.of_nat i) * step)%Q in if loc d e (xi,y) ltde then false else true) (PlotLine A p r step y d e ltde loc) end.
imports: QArith.Qround CoRN.metric2.Metric CoRN.metric2.ProductMetric CoRN.metric2.UniformContinuity CoRN.reals.fast.RasterizeQ CoRN.reals.fast.Interval CoRN.metric2.Graph CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax