aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules/obj.v
blob: b02bdf189d250b082ed3fd604364364949d89cea (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
Implicit Arguments On.

Mod M. 
  Definition a:=[s:Set]s.
  Print a.
EndM M.

Print M.a.

Mod K.
  Definition app:=[A,B:Set; f:(A->B); x:A](f x).
  Mod N.
    Definition apap:=[A,B:Set](app (app 1!A 2!B)).
    Print app.
    Print apap.
  EndM N.
  Print N.apap.
EndM K.

Print K.app.
Print K.N.apap.

Mod W:=K.N.

Print W.apap.