Quelle bug_2836.v Sprache: Coq

(* Check that possible instantiation made during evar materialization
   are taken into account and do not raise Not_found *)

Set Implicit Arguments.

Record SpecializedCategory (obj : Type) (Morphism : obj -> obj -> Type) := {
  Object :> _ := obj;

  Identity' : forall o, Morphism o o;
  Compose' : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
}.

Section SpecializedCategoryInterface.
  Variable obj : Type.
  Variable mor : obj -> obj -> Type.
  Variable C : @SpecializedCategory obj mor.

  Definition Morphism (s d : C) := mor s d.
  Definition Identity (o : C) : Morphism o o := C.(Identity') o.
  Definition Compose (s d d' : C) (m : Morphism d d') (m0 : Morphism s d) :
Morphism s d' := C.(Compose') s d d' m m0.
End SpecializedCategoryInterface.

Section ProductCategory.
  Variable objC : Type.
  Variable morC : objC -> objC -> Type.
  Variable objD : Type.
  Variable morD : objD -> objD -> Type.
  Variable C : SpecializedCategory morC.
  Variable D : SpecializedCategory morD.

(* Should fail nicely *)
Definition ProductCategory : @SpecializedCategory (objC * objD)%type (fun s d
=> (morC (fst s) (fst d) * morD (snd s) (snd d))%type).
Fail refine {|
      Identity' := (fun o => (Identity (fst o), Identity (snd o)));
      Compose' := (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd
m2) (snd m1)))
    |}.
Abort.
End ProductCategory.

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.