|
(* Example taken from RelationAlgebra *)
(* Was failing from r16205 up to now *)
Require Import BinNums.
Section A.
Context (A:Type) {X: A} (tst:A->Type) (top:forall X, X).
Inductive v: (positive -> A) -> Type :=
| v_L: forall f', v f'
| v_N: forall f',
v (fun n => f' (xO n)) ->
(positive -> tst (f' xH)) ->
v (fun n => f' (xI n)) -> v f'.
Fixpoint v_add f' (t: v f') n: (positive -> tst (f' n)) -> v f' :=
match t in (v o) return ((positive -> (tst (o n))) -> v o) with
| v_L f' =>
match n return ((positive -> (tst (f' n))) -> v f') with
| xH => fun x => v_N _ (v_L _) x (v_L _)
| xO n => fun x => v_N _
(v_add (fun n => f' (xO n)) (v_L _) n x) (fun _ => top _) (v_L _)
| xI n => fun x => v_N _
(v_L _) (fun _ => top _) (v_add (fun n => f' (xI n)) (v_L _) n x)
end
| v_N f' l y r =>
match n with
| xH => fun x => v_N _ l x r
| xO n => fun x => v_N _ (v_add (fun n => f' (xO n)) l n x) y r
| xI n => fun x => v_N _ l y (v_add (fun n => f' (xI n)) r n x)
end
end.
End A.
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
