Given
let multiplication_table =
0 -> 0 -> 0
+ 0 -> 1 -> 0
+ 1 -> 0 -> 0
+ 1 -> 1 -> 1
+ 0 -> 2 -> 0
+ 2 -> 0 -> 0
+ 2 -> 1 -> 2
+ 1 -> 2 -> 2
+ 2 -> 2 -> 4
then these two fun
s
fun mul_product_style: Int -> Int -> Int {
multiplication_table
}
fun mul_dereference_style[x, y: Int]: Int{
y::(x::(multiplication_table))
}
work exactly the same way at the call site,
run {
all x, y: {i: Int | 0 <= i && i < 2} | {
mul_product_style[x,y] = mul_dereference_style[x,y]
mul_product_style[x][y] = mul_dereference_style[x][y]
x::mul_product_style[y] = x::mul_dereference_style[y]
y::(x::mul_product_style) = y::(x::mul_dereference_style)
y.(x.mul_product_style) = y.(x.mul_dereference_style)
}
}
which suggests that they are the same relation. Questions:
- Why does
mul_dereference_style
not create a relation that may be interrogated in the evaluator whenmul_product_style
does? - Why does not
mul_product_style = mul_dereference_style
compile?
2.1 The error suggests that mul_dereference_style can only be applied and not used as a name, asmul_product_style
apparently can be, why this difference? -
fun mul_product_style: Int -> Int -> Int {multiplication_table}
does compile butfun mul_dereference_style[x, y: Int]: Int{ multiplication_table}
does not. It seems that the two functions in fact of dissimilar types, even though they work identically in therun
paragraph. Why so?