|
Set Implicit Arguments.
Require Import Logic.
Module NonPrim.
Local Set Nonrecursive Elimination Schemes.
Record prodwithlet (A B : Type) : Type :=
pair' { fst : A; fst' := fst; snd : B }.
Definition letreclet (p : prodwithlet nat nat) :=
let (x, x', y) := p in x + y.
Definition pletreclet (p : prodwithlet nat nat) :=
let 'pair' x x' y := p in x + y + x'.
Definition pletreclet2 (p : prodwithlet nat nat) :=
let 'pair' x y := p in x + y.
Check (pair 0 0).
End NonPrim.
Global Set Universe Polymorphism.
Global Set Asymmetric Patterns.
Local Set Nonrecursive Elimination Schemes.
Local Set Primitive Projections.
Record prod (A B : Type) : Type :=
pair { fst : A; snd : B }.
Print prod_rect.
(* What I really want: *)
Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B), P (pair fst snd))
(p : prod A B) : P p
:= u (fst p) (snd p).
Definition conv : @prod_rect = @prod_rect'.
Proof. reflexivity. Defined.
Definition imposs :=
(fun A B P f (p : prod A B) => match p as p0 return P p0 with
| {| fst := x ; snd := x0 |} => f x x0
end).
Definition letrec (p : prod nat nat) :=
let (x, y) := p in x + y.
Eval compute in letrec (pair 1 5).
Goal forall p : prod nat nat, letrec p = fst p + snd p.
Proof.
reflexivity.
Undo.
intros p.
case p. simpl. unfold letrec. simpl. reflexivity.
Defined.
Eval compute in conv. (* = eq_refl
: prod_rect = prod_rect' *)
Check eq_refl : @prod_rect = @prod_rect'. (* Toplevel input, characters 6-13:
Error:
The term "eq_refl" has type "prod_rect = prod_rect"
while it is expected to have type "prod_rect = prod_rect'"
(cannot unify "prod_rect" and "prod_rect'"). *)
Record sigma (A : Type) (B : A -> Type) : Type :=
dpair { pi1 : A ; pi2 : B pi1 }.
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.37Angebot
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
|
