Quelle ImplicitArguments.v Sprache: Coq

Axiom foo : forall (x y z t : nat), nat.

Arguments foo {_} _ [z] t.
Check (foo 1).
Arguments foo {_} _ {z} {t}.
Fail Arguments foo {_} _ [z] {t}.
Check (foo 1).

Definition foo1 [m] n := n + m.
Check (foo1 1).

Inductive vector {A : Type} : nat -> Type :=
| vnil : vector 0
| vcons : A -> forall {n'}, vector n' -> vector (S n').

Arguments vector A : clear implicits.

Require Import TestSuite.jmeq.

Definition head_subproof A n (v : vector A (S n)) (a : A) n'
    (v' : vector A n') (eqn : S n' = S n) (eqv : JMeq (vcons a v') v) :=
  let H : S n = S n -> n' = n :=
    match eqn in _ = n'' return n'' = S n -> n' = n with
    | eq_refl =>
        fun eqSn' : S n' = S n =>
          let eqn' : n' = n :=
            f_equal (fun e => match e with  0 => n' | S n0 => n0 end) eqSn' in
          eq_ind_r (fun n'' => n'' = n)
            (eq_ind_r
               (fun n' =>
                  forall v', S n' = S n -> JMeq (vcons a v') v -> n = n)
               (fun (v' : vector A n) _ _ => eq_refl) eqn' v'
               eqn eqv)
            eqn'
    end in
  H eq_refl.

Definition head {A : Type} {n : nat} (v : vector A (S n)) :=
  let case_nil (eqn : O = S n) _ :=
    False_rect (vector A n)
      (False_ind False
         (eq_ind O (fun e => match e with O => True | S _ => False end)
            I (S n) eqn)) in
  let case_cons (a : A) n' (v' : vector A n')
        (eqn : eq (S n') (S n)) (eqv : JMeq (vcons a v') v) :=
      eq_rect n' (vector A) v' n
        (head_subproof A n v a n' v' eqn eqv) in
  match
    v as v' in vector _ n' return eq n' (S n) -> JMeq v' v -> vector A n
  with
  | vnil => case_nil
  | @vcons _ a n' v' => case_cons a n' v'
  end (eq_refl (S n)) (JMeq_refl v).

Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A (n + m) :=
  match v in vector _ n return vector A (n + m) with
    | vnil => w
    | vcons a v' => vcons a (app v' w)
  end.

(* Test sharing information between different hypotheses *)

Parameters (a:_) (b:a=0).

(* These examples were failing due to a lifting wrongly taking let-in into account *)

Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.

Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
Abort.

(* Some example which should succeed with local implicit arguments *)

Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A.
Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P.

Inductive A' {P:forall m [n], n=m -> Prop} := C' : P 0 eq_refl -> A'.
Inductive A'' [P:forall m {n}, n=m -> Prop] (b : bool):= C'' : P 0 eq_refl -> A'' b.
Inductive A''' (P:forall m [n], n=m -> Prop) (b : bool):= C''' : P 0 eq_refl -> A''' P b.

Definition F (id: forall [A] [x : A], A) := id.
Definition G := let id := (fun [A] (x : A) => x) in id.
Fail Definition G' := let id := (fun {A} (x : A) => x) in id.

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.