test-suite/modules/grammar.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

Mod N.
Definition f:=plus.
Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E].
Check (f O O).
EndM N.
Check (N.f O O).
Imp N.
Check (N.f O O).
Check (f O O).
Mod M:=N.
Check (f O O).
Check (N.f O O).
Imp M.
Check (f O O).
Check (N.f O O).