Quelle bug_19082.v Sprache: Coq

Inductive boring1 := Boring1.
Inductive boring2 := Boring2.

Inductive output_wrapper := OutputWrapper {
    ow_alice : boring1;
}.

#[projections(primitive)]
Inductive request := InputWrapper {
    req_alice : boring1;
    req_next_bob := Boring2;
}.

Definition do_the_thing (req : request) : output_wrapper.
Proof.
  exact (
      match req with
      | {|
          req_alice := alice;
       |} =>
        OutputWrapper alice
      end
  ).
  Validate Proof.
Qed.

quality100%

¤ Dauer der Verarbeitung: 0.5 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.