Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_3343.v Sprache: Coq

Original von: Coq^©

(* File reduced by coq-bug-finder from original input, then from 13699 lines to 656 lines, then from 584 lines to 200 lines *)
Set Asymmetric Patterns.
Require Export Coq.Lists.List.
Export List.ListNotations.

Record CFGV := { Terminal : Type; VarSym : Type }.

Section Gram.
  Context  {G : CFGV}.

  Inductive  Pattern : (Terminal G) -> Type :=
  | ptleaf : forall (T : Terminal G),
               nat -> Pattern T
  with Mixture : list (Terminal G) -> Type :=
  | mtcons : forall {h: Terminal G}
                    {tl: list (Terminal G)},
               Pattern h -> Mixture tl -> Mixture (h::tl).

  Variable vc : VarSym G.

  Fixpoint pBVars {gs}  (p : Pattern gs) : (list nat) :=
    match p with
      | ptleaf _ _ => []
    end
  with mBVars {lgs} (pts : Mixture lgs) : (list nat) :=
         match pts with
           | mtcons _ _ _ tl =>  mBVars  tl
         end.

  Lemma mBndngVarsAsNth :
    forall mp (m : @Mixture mp),
      mBVars m = [2].
  Proof.
    intros.
    induction m. progress simpl.
  Admitted.
End Gram.

Lemma mBndngVarsAsNth' {G : CFGV} { vc  : VarSym G} :
  forall mp (m : @Mixture G mp),
    mBVars m = [2].
Proof.
  intros.
  induction m.
  Fail progress simpl.
  (* simpl did nothing here, while it does something inside the section; this is probably a bug*)
Abort.

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.