Перевод VDM в Изабель

Question

Я пытаюсь перевести модель VDM на Изабель, но почему-то, что я делаю, не работает

Следующий пример - функция VDM моей модели

    Dot_Move_invariant: Dot * Dot -> bool
Dot_Move_invariant(d1, d2) ==
    d1 < d2 and
    let coordinate_1 = Dot_Coord(d1) in
    let coordinate_2 = Dot_Coord(d2) in
    moving_coordinates_invariant(coordinate_1, coordinate_2);

И следующий пример представляет мою попытку перевести это

  definition
  Dot_Move_invariant:: "Dot⇒Dot⇒"
  where "Dot_Move_invariant d1 d2 ≡ d1 < d2 ∧  let x = (SOME y. y ∈ Dot_Coord d1) in x ∧ let y = (SOME x. x ∈ Dot_Coord d2 ) "

Я получаю ошибку: Внутренняя синтаксическая ошибка⌂ Не удалось разобрать проп

Answer 1

Это может быть следующим:

"Dot_Move_invariant d1 d2 ≡ d1 < d2 ∧ let x = (SOME y. y ∈ Dot_Coord d1) in x ∧ let y = (SOME x. x ∈ Dot_Coord d2 ) in y"