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 funs
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_stylenot create a relation that may be interrogated in the evaluator whenmul_product_styledoes? - Why does not
mul_product_style = mul_dereference_stylecompile?
2.1 The error suggests that mul_dereference_style can only be applied and not used as a name, asmul_product_styleapparently 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 therunparagraph. Why so?