Quelle bug_19661.v Sprache: Coq

Inductive tele : Type :=
  | TeleO : tele
  | TeleS {X} (binder : X -> tele) : tele.

Fixpoint tele_fun (TT : tele) (T : Type) : Type :=
  match TT with
  | TeleO => T
  | TeleS b => forall x, tele_fun (b x) T
  end.

Notation "TT -t> A" := (tele_fun TT A) (at level 99, A at level 200, right associativity).

Record tele_arg_cons {X : Type} (f : X -> Type) : Type := TeleArgCons
  { tele_arg_head : X;
    tele_arg_tail : f tele_arg_head }.
Global Arguments TeleArgCons {_ _} _ _.

Fixpoint tele_arg (t : tele) : Type :=
  match t with
  | TeleO => unit
  | TeleS f => tele_arg_cons (fun x => tele_arg (f x))
  end.

Fixpoint tele_app {TT : tele} {U} : (TT -t> U) -> tele_arg TT -> U :=
  match TT as TT return (TT -t> U) -> tele_arg TT -> U with
  | TeleO => fun F _ => F
  | TeleS r => fun (F : TeleS r -t> U) '(TeleArgCons x b) =>
      tele_app (F x) b
  end.
Global Arguments tele_app {!_ _} & _ !_ /.

Axiom PROP: Type.
Axiom T : PROP.
Axiom atomic_commit :
  forall {TB : tele}
         (_ : forall (_ : tele_arg TB), PROP)
         (_ : forall (_ : tele_arg TB), PROP),
    PROP.

Fixpoint do_after_shatter  (next : nat) (d : nat) : PROP :=
  match d with
  | 0 => T
  | S d =>
  (@atomic_commit
      (@TeleS _ (fun l' => TeleO))
      ((@tele_app (@TeleS _ (fun l' => TeleO))
          _ (fun l' => T)))
      ((@tele_app (@TeleS _ (fun l' =>  TeleO))
          _ (fun l' =>
                      do_after_shatter (l'-1) d
                    ))))
  end.

quality99%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

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.