File: bug_20124_1.v

package info (click to toggle)
coq 9.1.0%2Bdfsg-3
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 35,964 kB
  • sloc: ml: 239,908; sh: 4,355; python: 2,985; ansic: 2,644; makefile: 874; lisp: 171; javascript: 63; xml: 24; sed: 2
file content (23 lines) | stat: -rw-r--r-- 468 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
 
Module Type MiniOrderedType.
  Parameter Inline t : Type.
End MiniOrderedType.

Module Type L_Struct.
  Declare Module FOrd : MiniOrderedType.
End L_Struct.

Module Type ST_Struct.
  Declare Module L : L_Struct.
End ST_Struct.

Module CP_beta_eta (L_ : L_Struct).
  Module L := L_.
End CP_beta_eta.

Module Make (ST : ST_Struct) (CP : ST_Struct with Module L := ST.L).

End Make.

Declare Module ST : ST_Struct.
Module CP := CP_beta_eta ST.L.
Module SN := Make ST CP.