|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Sprache: Unknown
Columbo aufrufen.out zum Wurzelverzeichnis wechselnHaskell {Haskell[306] Ada[597] Abap[738]}Datei anzeigen
le_n: forall n : nat, n <= n
le_0_n: forall n : nat, 0 <= n
le_S: forall n m : nat, n <= m -> n <= S m
le_S_n: forall n m : nat, S n <= S m -> n <= m
le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
le_n_S: forall n m : nat, n <= m -> S n <= S m
max_l: forall n m : nat, m <= n -> Nat.max n m = n
max_r: forall n m : nat, n <= m -> Nat.max n m = m
min_r: forall n m : nat, m <= n -> Nat.min n m = m
min_l: forall n m : nat, n <= m -> Nat.min n m = n
le_ind:
forall (n : nat) (P : nat -> Prop),
P n ->
(forall m : nat, n <= m -> P m -> P (S m)) ->
forall n0 : nat, n <= n0 -> P n0
le_sind:
forall (n : nat) (P : nat -> SProp),
P n ->
(forall m : nat, n <= m -> P m -> P (S m)) ->
forall n0 : nat, n <= n0 -> P n0
false: bool
true: bool
eq_true: bool -> Prop
is_true: bool -> Prop
negb: bool -> bool
andb: bool -> bool -> bool
orb: bool -> bool -> bool
implb: bool -> bool -> bool
xorb: bool -> bool -> bool
Nat.even: nat -> bool
Nat.odd: nat -> bool
BoolSpec: Prop -> Prop -> bool -> Prop
Nat.ltb: nat -> nat -> bool
Nat.testbit: nat -> nat -> bool
Nat.eqb: nat -> nat -> bool
Nat.leb: nat -> nat -> bool
Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
eq_true_ind_r:
forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
eq_true_rec:
forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
eq_true_rect:
forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
eq_true_sind:
forall P : bool -> SProp, P true -> forall b : bool, eq_true b -> P b
bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
eq_true_ind:
forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
eq_true_rec_r:
forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
eq_true_rect_r:
forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
bool_sind:
forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
Byte.to_bits:
Byte.byte ->
bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
Byte.of_bits:
bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
Byte.byte
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
andb_true_intro:
forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
BoolSpec_sind:
forall (P Q : Prop) (P0 : bool -> SProp),
(P -> P0 true) ->
(Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
BoolSpec_ind:
forall (P Q : Prop) (P0 : bool -> Prop),
(P -> P0 true) ->
(Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
Byte.to_bits_of_bits:
forall
b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
Byte.to_bits (Byte.of_bits b) = b
bool_choice:
forall (S : Set) (R1 R2 : S -> Prop),
(forall x : S, {R1 x} + {R2 x}) ->
{f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
mult_n_O: forall n : nat, 0 = n * 0
plus_O_n: forall n : nat, 0 + n = n
plus_n_O: forall n : nat, n = n + 0
n_Sn: forall n : nat, n <> S n
pred_Sn: forall n : nat, n = Nat.pred (S n)
O_S: forall n : nat, 0 <> S n
f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
eq_S: forall x y : nat, x = y -> S x = S y
eq_add_S: forall n m : nat, S n = S m -> n = m
min_r: forall n m : nat, m <= n -> Nat.min n m = m
min_l: forall n m : nat, n <= m -> Nat.min n m = n
max_r: forall n m : nat, n <= m -> Nat.max n m = m
max_l: forall n m : nat, m <= n -> Nat.max n m = n
plus_Sn_m: forall n m : nat, S n + m = S (n + m)
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
not_eq_S: forall n m : nat, n <> m -> S n <> S m
mult_n_Sm: forall n m : nat, n * m + n = n * S m
f_equal2_plus:
forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
f_equal2_mult:
forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
f_equal2_nat:
forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
andb_true_intro:
forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
bool_choice:
forall (S : Set) (R1 R2 : S -> Prop),
(forall x : S, {R1 x} + {R2 x}) ->
{f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
andb_true_intro:
forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
h: n <> newdef n
h': newdef n <> n
h: n <> newdef n
h': newdef n <> n
h: n <> newdef n
h: n <> newdef n
h: n <> newdef n
h': newdef n <> n
The command has indeed failed with message:
No such goal.
The command has indeed failed with message:
Query commands only support the single numbered goal selector.
The command has indeed failed with message:
Query commands only support the single numbered goal selector.
h: P n
h': ~ P n
h: P n
h': ~ P n
h: P n
h': ~ P n
h: P n
h: P n
[ Original von:0.107Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen.
Man kann per Verzeichnistruktur darin navigieren.
Der Code wird farblich markiert angezeigt.
]
|
|
|
|
|
|
