blob: fb734b5d5936a83a17f6513bcc52daf42de70c4c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Module N.
Definition f:=plus.
Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E].
Check (f O O).
End N.
Check (N.f O O).
Import N.
Check (N.f O O).
Check (f O O).
Module M:=N.
Check (f O O).
Check (N.f O O).
Import M.
Check (f O O).
Check (N.f O O).
|
