File: obj.v

package info (click to toggle)
coq 8.16.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 40,596 kB
  • sloc: ml: 219,376; sh: 3,545; python: 3,231; ansic: 2,529; makefile: 767; lisp: 279; javascript: 63; xml: 24; sed: 2
file content (26 lines) | stat: -rw-r--r-- 386 bytes parent folder | download | duplicates (12) 
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
 
Set Implicit Arguments.
Unset Strict Implicit.

Module M.
  Definition a (s : Set) := s.
  Print a.
End M.

Print M.a.

Module K.
  Definition app (A B : Set) (f : A -> B) (x : A) := f x.
  Module N.
    Definition apap (A B : Set) := app (app (A:=A) (B:=B)).
    Print app.
    Print apap.
  End N.
  Print N.apap.
End K.

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

Module W := K.N.

Print W.apap.