|
Definition MR {T M : Type} :=
fun (R : M -> M -> Prop) (m : T -> M) (x y : T) => R (m x) (m y).
Set Primitive Projections.
Record sigma {A : Type} {B : A -> Type} : Type := sigmaI
{ pr1 : A; pr2 : B pr1 }.
Axiom F : forall {A : Type} {R : A -> A -> Prop},
(forall x, (forall y, R y x -> unit) -> unit) -> forall (x : A), unit.
Definition foo (A : Type) (l : list A) :=
let y := {| pr1 := A; pr2 := l |} in
let bar := MR lt (fun p : sigma =>
(fix Ffix (x : list (pr1 p)) : nat :=
match x with
| nil => 0
| cons _ x1 => S (Ffix x1)
end) (pr2 p)) in
fun (_ : bar y y) =>
F (fun (r : sigma)
(X : forall q : sigma, bar q r -> unit) => tt).
Definition fooT (A : Type) (l : list A) : Type :=
ltac:(let ty := type of (foo A l) in exact ty).
Parameter P : forall A l, fooT A l -> Prop.
Goal forall A l, P A l (foo A l).
Proof.
intros; unfold foo.
Fail match goal with
| [ |- context [False]] => idtac
end.
Admitted.
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
