diff options
Diffstat (limited to 'test-suite/output/Implicit.v')
| -rw-r--r-- | test-suite/output/Implicit.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index 0ff7e87f..4c6f2b5d 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -17,3 +17,22 @@ Definition d1 y x (h : x = y :>nat) := h. Definition d2 x := d1 (y:=x). Print d2. + +(* Check maximal insertion of implicit *) + +Require Import List. + +Open Scope list_scope. + +Set Implicit Arguments. +Set Maximal Implicit Insertion. + +Definition id (A:Type) (x:A) := x. + +Check map id (1::nil). + +Definition id' (A:Type) (x:A) := x. + +Implicit Arguments id' [[A]]. + +Check map id' (1::nil). |