Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: completion_popup.scala Sprache: Coq

Original von: Coq^©

Set Implicit Arguments.

Require Import Logic.

Set Asymmetric Patterns.
Set Nonrecursive Elimination Schemes.
Set Primitive Projections.

Record prod (A B : Type) : Type :=
  pair { fst : A; snd : B }.

Print prod_rect.
(** prod_rect =
fun (A B : Type) (P : prod A B -> Type)
  (f : forall (fst : A) (snd : B), P {| fst := fst; snd := snd |})
  (p : prod A B) =>
match p as p0 return (P p0) with
| {| fst := x; snd := x0 |} => f x x0
end
     : forall (A B : Type) (P : prod A B -> Type),
       (forall (fst : A) (snd : B), P {| fst := fst; snd := snd |}) ->
       forall p : prod A B, P p

Arguments A, B are implicit
Argument scopes are [type_scope type_scope _ _ _]
*)

(* What I really want: *)
Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B), P (pair fst snd))
           (p : prod A B) : P p
  := u (fst p) (snd p).

Notation typeof x := (ltac:(let T := type of x in exact T)) (only parsing).

(* Check for eta *)
Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect').

(* Check for the recursion principle I want *)
Check eq_refl : @prod_rect = @prod_rect'.

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.