You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardexpand all lines: examples/hyperrec/spec2.vcl
+11-17
Original file line number
Diff line number
Diff line change
@@ -55,22 +55,22 @@ inputTranspose = foreach i . foreach j . inputs ! j ! i
55
55
-- identity : Tensor Rat [2, 3]
56
56
-- identity = [ [1, 0, 1], [0, 1, 0] ]
57
57
58
-
-- vectorMin : Tensor Rat [inputSize, 5] -> Index 5 -> Bool
59
-
-- vectorMin x i = forall j k. x ! j ! i <= x ! j ! k
58
+
-- vectorMin : Tensor Rat [inputSize, 5] -> Index 5 -> Bool
59
+
-- vectorMin x i = forall j k. x ! j ! i <= x ! j ! k
60
60
61
61
vectorMin : Index 30 -> Index 5 -> Bool
62
-
vectorMin i j = forall k . inputs ! j ! i <= inputs ! j ! k
62
+
vectorMin i j = forall k . inputs ! j ! i <= inputs ! j ! k
63
63
64
64
vectorMax : Index 30 -> Index 5 -> Bool
65
-
vectorMax i j = forall k . inputs ! j ! k <= inputs ! j ! i
65
+
vectorMax i j = forall k . inputs ! j ! k <= inputs ! j ! i
66
66
67
67
@property
68
68
property : Bool
69
-
property = forall x. forall j i l k. validInput x and vectorMin i j and vectorMax l k and x ! i >= inputs ! j ! i and inputs ! k ! l >= x ! l => advises x pos
69
+
property = forall x. forall j i l k. validInput x and vectorMin i j and vectorMax l k and x ! i >= inputs ! j ! i and inputs ! k ! l >= x ! l => advises x pos
70
70
71
71
{-
72
-
vectorMax : Vector Rat 5 -> Index 5 -> Vector Bool 5
73
-
vectorMax x i = foreach j . x ! j <= x ! i
72
+
vectorMax : Vector Rat 5 -> Index 5 -> Vector Bool 5
73
+
vectorMax x i = foreach j . x ! j <= x ! i
74
74
75
75
vectorOut : Tensor Rat [inputSize, n] -> Vector Rat inputSize
76
76
vectorOut x = foreach i . x ! i -}
@@ -80,25 +80,19 @@ vectorOut x = foreach i . x ! i -}
0 commit comments