91 (1) equalities eqs [[ eqs ]] [[ eqs ]] |
91 (1) equalities eqs [[ eqs ]] [[ eqs ]] |
92 (2) equalities [c_2 = 0, L *..] [[ [c_2 = 0], [L *..] ]] [[ [c_2 = 0], [L *..] ]] |
92 (2) equalities [c_2 = 0, L *..] [[ [c_2 = 0], [L *..] ]] [[ [c_2 = 0], [L *..] ]] |
93 (3) solveForVars [c, c_2, c_3] [[ [c], [c_2], [c_3] ]] [[ [c], [c_2], [c_3] ]] |
93 (3) solveForVars [c, c_2, c_3] [[ [c], [c_2], [c_3] ]] [[ [c], [c_2], [c_3] ]] |
94 (4) Constants [r = 7] [[ [[r = 7]] ]] [[ [[r = 7]] ]] |
94 (4) Constants [r = 7] [[ [[r = 7]] ]] [[ [[r = 7]] ]] |
95 (5) Maximum A [[ A ]] [[ A ]] |
95 (5) Maximum A [[ A ]] [[ A ]] |
96 ---> fun make_values (descr, ts) --> |
96 ---> Model_Def.make_values (descr, ts) --> |
97 <--- fun make_present (descr, ts) <-- |
97 <--- Model_Def.values_to_present ctxt (descr, ts) <-- |
98 |
98 |
99 Observe the elements of HOL-lists enclosed in ML-lists in lines (2..4). |
99 Observe the elements of HOL-lists enclosed in ML-lists in lines (2..4). |
100 Without those (strange!) HOL-lists in values one could not distinguish (1) and (3), |
100 Without those (strange!) HOL-lists in values one could not distinguish (1) and (3), |
101 in case ony one element is input ("Inc (solveForVars c)") |
101 in case ony one element is input ("Inc (solveForVars c)") |
102 and the representation to the user could not distinguish between "c" and "[c]"; |
102 and the representation to the user could not distinguish between "c" and "[c]"; |