Quelle constr.v Sprache: Coq

Require Import Ltac2.Constr Ltac2.Init Ltac2.Control.
Import Unsafe.

Ltac2 Eval match (kind '(nat -> bool)) with
           | Prod a c => a
           | _ => throw Match_failure end.

Set Allow StrictProp.
Axiom something : SProp.
Ltac2 Eval match (kind '(forall x : something, bool)) with
           | Prod a c => a
           | _ => throw Match_failure end.

From Corelib Require Import PrimInt63 PrimArray.
Open Scope array_scope.
Ltac2 Eval match (kind '([|true|true|])) with
  | Array _ _ _ ty => ty
  | _ => throw Match_failure end.

quality99%

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