Изабель решает толкование

Question

Я использую Изабель 2019 и у меня возникли некоторые проблемы с местными жителями:

Я строю локаль с сокращением, например:

interpretation myInstance : myLocale "abbreviation"

Я использую это с функция из локали, например:

myInstance.getter myinput

Но apply simp теперь "упрощает" цель до чего-то подобного

myLocale.getter "abbreviation" myinput

Как можно избежать упрощения, чтобы сделать это? (Я почти уверен, что это причина того, почему мой код обрабатывается очень долго) ...

Best

Answer 1

Это известная проблема , и не существует идеального решения. Некоторые частичные решения:

• жить с этим / избегать использования чего-то, что может быть упрощено. Используйте определение вместо аббревиатуры (и в конечном итоге пометьте определение как простое, чтобы автоматически развернуть его).

• добавить правило конгруэнтности (как упомянуто ): ⋀a b. myLocale.getter a b == myLocale.getter "abbreviation" myinput a b. Это не всегда работает.

• Определите новую константу и поднимите все теоремы до этой константы. Это раздражает (и может сделать кувалду менее мощным).