File: notation.ref

package info (click to toggle)
coq-stdpp 1.11.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 1,696 kB
  • sloc: makefile: 52; sh: 35; sed: 1
file content (35 lines) | stat: -rw-r--r-- 1,009 bytes parent folder | download | duplicates (2)
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
27
28
29
30
31
32
33
34
35
test_2 = {[10 := {[10 := 1]}; 20 := {[20 := 2]}]}
     : M (M nat)
test_3 =
{[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}]}
     : M (M nat)
test_4 =
{[10 := {[10 := 1]}; 20 := {[20 := 2]}; 30 := {[30 := 3]}; 40 := {[40 := 4]}]}
     : M (M nat)
test_op_2 =
{[10 := {[10 ^ 2 := 99]}; 10 + 1 := {[10 - 100 := 42 * 1337]}]}
     : M (M nat)
test_op_3 =
{[10 := {[20 - 2 := [11]; 1 := [22]]};
  20 := {[99 + length [1] := [1; 2; 3]]};
  4 := {[4 := [4]]};
  5 := {[5 := [5]]}]}
     : M (M (list nat))
test_op_4 =
{[10 := {[20 - 2 := [11];
          1 := [22];
          3 := [23];
          4 := [1; 2; 3; 4; 5; 6; 7; 8; 9]]};
  20 := {[99 + length [1] := [1; 2; 3]]};
  4 := {[4 := [4]]};
  5 := {[5 := [5]]}]}
     : M (M (list nat))
test_gmultiset_1 = {[+ 10 +]}
     : gmultiset nat
test_gmultiset_2 = {[+ 10; 11 +]}
     : gmultiset nat
test_gmultiset_3 = {[+ 10; 11; 2 - 2 +]}
     : gmultiset nat
test_gmultiset_4 =
{[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]}
     : gmultiset (gmultiset nat)