Идрис не уменьшает поиск по карте
Я угадаю ошибку. Кажется, вы не указали свою переменную vol. Каждая переменная должна быть объявлена с его типом, который будет использоваться в Java. Я также предполагаю, что вам нужно показать результат с фиксированной десятичной точкой из двух.
Итак, в коде у вас должно быть что-то вроде:
void display()
{
float vol= (float)(l*b*h);
String strVol = String.format("%.2f", vol);
System.out.println("Volume is:"+ strVol );
}
См. Формат Float to n decimal для помощи в форматировании вашего значения.
Кроме того, в вашем основном методе вы используете объект cube, когда вы объявили объект / класс cubeVol. Еще раз просмотрите свои ошибки!
PD: Как уже указывалось в комментариях, вы не сказали, в чем вопрос и какая у вас ошибка. (У меня ошибка при компиляции, при запуске консоли отображается ошибка, программа не очень хорошо вычисляет и т. Д.). Пожалуйста, отредактируйте и уточните свой пост.
1 ответ
Он должен иметь что-то общее с реализацией SortedMap, так как версия, использующая простую List, работает, как и ожидалось:
N : List (String, Type)
N =
[ ("a", Nat)
, ("b", String)
]
t : lookup "a" N = Just Nat
t = Refl
Согласно документам Data.SortedMap.lookup также является полной, поэтому это должно уменьшить. Возможно, причина в том, что функции и типы данных в SortedMap, похоже, имеют спецификатор экспорта, тогда как в Data.List используются public export.