(* Check discharge of arguments scopes + other checks *)
(* This is bug #4865 *)
Notation"" := true : bool_scope. Section A. Check negb <T>. GlobalArguments negb : clear scopes.
Fail Check negb <T>. End A.
(* Check that no scope is re-computed *)
Fail Check negb <T>.
(* Another test about arguments scopes in sections *)
Notation"0" := true. Section B. Variable x : nat. Let T := nat -> nat. Definition f y : T := fun z => x + y + z.
Fail Check f 1 0. (* 0 in nat, 0 in bool *)
Fail Check f 0 0. (* 0 in nat, 0 in bool *) Check f 0 1. (* 0 and 1 in nat *) GlobalArguments f _%_nat_scope _%_nat_scope. Check f 0 0. (* both 0 in nat *) End B.
(* Check that only the scope for the extra product on x is re-computed *) Check f 0 0 0. (* All 0 in nat *)
Section C. Variable x : nat. Let T := nat -> nat. Definition g y : T := fun z => x + y + z. GlobalArguments g : clear scopes. Check g 1. (* 1 in nat *) End C.
(* Check that only the scope for the extra product on x is re-computed *) Check g 0. (* 0 in nat *)
Fail Check g 0 1 0. (* 2nd 0 in bool *)
Fail Check g 0 0 1. (* 2nd 0 in bool *)
(* Another test on arguments scopes: checking scope for expanding arities *) (* Not sure this is very useful, but why not *)
Fixpoint arr n := match n with 0%nat => nat | S n => nat -> arr n end. Fixpoint lam n : arr n := match n with 0%nat => 0%nat | S n => fun x => lam n end. Notation"0" := true. Arguments lam _%_nat_scope _%_nat_scope : extra scopes. Check (lam 1 0).
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.
