aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Projection.v
blob: 3ffd41ea07d85965cdc31032ab70329d6b5e5b75 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
Record foo (A : Type) := { B :> Type }.

Lemma bar (f : foo nat) (x : f) : x = x.
  destruct f. simpl B. simpl B in x.
Abort.

Structure S : Type :=  {Dom : Type; Op : Dom -> Dom -> Dom}.

Check (fun s : S => Dom s).
Check (fun s : S => Op s).
Check (fun (s : S) (a b : Dom s) => Op s a b).

(* v8
Check fun s:S => s.(Dom).
Check fun s:S => s.(Op).
Check fun (s:S) (a b:s.(Dom)) => s.(Op) a b.
*)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Strict Implicit.

Structure S' (A : Set) : Type :=  {Dom' : Type; Op' : A -> Dom' -> Dom'}.

Check (fun s : S' nat => Dom' s).
Check (fun s : S' nat => Op' (s:=s)).
Check (fun s : S' nat => Op' (A:=nat) (s:=s)).
Check (fun (s : S' nat) (a : nat) (b : Dom' s) => Op' a b).
Check (fun (s : S' nat) (a : nat) (b : Dom' s) => Op' (A:=nat) (s:=s) a b).

(* v8
Check fun s:S' => s.(Dom').
Check fun s:S' => s.(Op').
Check fun (s:S') (a b:s.(Dom')) => _.(Op') a b.
Check fun (s:S') (a b:s.(Dom')) => s.(Op') a b.

Set Implicit Arguments.
Unset Strict Implicits.

Structure S' (A:Set) : Type :=
 {Dom'     : Type;
  Op'      : A -> Dom' -> Dom'}.

Check fun s:S' nat => s.(Dom').
Check fun s:S' nat => s.(Op').
Check fun (s:S' nat) (a:nat) (b:s.(Dom')) => _.(@Op' nat) a b.
Check fun (s:S' nat) (a:nat) (b:s.(Dom')) => s.(Op') a b.
*)