|
Module Type TITI.
Parameter B:Set.
Parameter x:B.
Inductive A:Set:=
a1:B->A.
Definition f2: A ->B
:= fun (a:A) =>
match a with
(a1 b)=>b
end.
Definition f: A -> B:=fun (a:A) => x.
End TITI.
Module Type TIT.
Declare Module t:TITI.
End TIT.
Module Seq(titi:TIT).
Module t:=titi.t.
Inductive toto:t.A->t.B->Set:=
t1:forall (a:t.A), (toto a (t.f a))
| t2:forall (a:t.A), (toto a (t.f2 a)).
End Seq.
Module koko(tit:TIT).
Module seq:=Seq tit.
Module t':=tit.t.
Definition def:forall (a:t'.A), (seq.toto a (t'.f a)).
intro ; constructor 1.
Defined.
Definition def2: forall (a:t'.A), (seq.toto a (t'.f2 a)).
intro; constructor 2.
(* Toplevel input, characters 0-13
constructor 2.
^^^^^^^^^^^^^
Error: Impossible to unify (seq.toto ?3 (seq.t.f2 ?3)) with
(seq.toto a (t'.f2 a)).*)
Abort.
End koko.
¤ Dauer der Verarbeitung: 0.15 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.
|
