| products/sources/formale Sprachen/Coq/test-suite/success/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Prinzipien der Anforderungsanalyse bug_4205.v Sprache: CoqOriginal von: Coq© |
|
||||||
|
Inductive even (x : bool) : nat -> Type :=
| evenO : even x 0 | evenS : forall n, odd x n -> even x (S n) with odd (x : bool) : nat -> Type := | oddS : forall n, even x n -> odd x (S n). Scheme even_ind_prop := Induction for even Sort Prop with odd_ind_prop := Induction for odd Sort Prop. Combined Scheme even_cprop from even_ind_prop, odd_ind_prop. Check even_cprop : forall (x : bool) (P : forall n : nat, even x n -> Prop) (P0 : forall n : nat, odd x n -> Prop), P 0 (evenO x) -> (forall (n : nat) (o : odd x n), P0 n o -> P (S n) (evenS x n o)) -> (forall (n : nat) (e : even x n), P n e -> P0 (S n) (oddS x n e)) -> (forall (n : nat) (e : even x n), P n e) /\ (forall (n : nat) (o : odd x n), P0 n o). Scheme even_ind_type := Induction for even Sort Type with odd_ind_type := Induction for odd Sort Type. (* This didn't work in v8.7 *) Combined Scheme even_ctype from even_ind_type, odd_ind_type. Check even_ctype : forall (x : bool) (P : forall n : nat, even x n -> Prop) (P0 : forall n : nat, odd x n -> Prop), P 0 (evenO x) -> (forall (n : nat) (o : odd x n), P0 n o -> P (S n) (evenS x n o)) -> (forall (n : nat) (e : even x n), P n e -> P0 (S n) (oddS x n e)) -> (forall (n : nat) (e : even x n), P n e) * (forall (n : nat) (o : odd x n), P0 n o). ¤ Dauer der Verarbeitung: 0.30 Sekunden (vorverarbeitet) ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
