История изменений
Исправление AndreyKl, (текущая версия) :
Как то так (в фигурных скобках неявный параметр, он должен выводиться из контекста).
gt_trans : {z : double} -> (x : double) -> (prf : x > y) -> {y > z} -> (x > z)
gt_dec : (x y : double) -> Either (x > y) (x <= y)
f : (x : Double) -> (prf : x > -273.5) -> Double
g x = if gt_dec x -50 == Left prf
then
f x (gt_trans x prf )
else
x
Функции вроде gt_trans , congr - часть стандартной библиотеки или около того.
g1 = if x > -300 then f x else x
Не скомпилируется потому что не найдёт доказателство что x > -273.5.
Исправление AndreyKl, :
Как то так (в фигурных скобках неявный параметр, он должен выводиться из контекста).
gt_trans : {z : double} -> (x : double) -> (prf : x > y) -> (y > z) -> (x > z)
gt_dec : (x y : double) -> Either (x > y) (x <= y)
f : (x : Double) -> (prf : x > -273.5) -> Double
g x = if gt_dec x -50 == Left prf
then
f x (gt_trans x prf)
else
x
Функции вроде gt_trans , congr - часть стандартной библиотеки или около того.
g1 = if x > -300 then f x else x
Не скомпилируется потому что не найдёт доказателство что x > -273.5.
Исправление AndreyKl, :
Как то так (в фигурных скобках неявный параметр, он должен выводиться из контекста).
gt_trans : {z : double} (x : double) -> (prf : x > y) -> (y > z) -> (x > z)
gt_dec : (x y : double) -> Either (x > y) (x <= y)
f : (x : Double) -> (prf : x > -273.5) -> Double
g x = if gt_dec x -50 == Left prf
then
f x (gt_trans x prf)
else
x
Функции вроде gt_trans , congr - часть стандартной библиотеки или около того.
g1 = if x > -300 then f x else x
Не скомпилируется потому что не найдёт доказателство что x > -273.5.
Исправление AndreyKl, :
Как то так (в фигурных скобках неявный параметр, он должен выводиться из контекста).
gt_trans : {z : double} (x : double) -> (prf : x > y) -> (y > z) -> (x > z)
gt_dec : (x y : double) -> Either (x > y) (x <= y)
f : (x : Double) -> (prf : x > -273.5) -> Double
g x = if gt_dec x -50 == Left prf
then
f x (gt_trans x prf)
else
x
Функции вроде gt_trans , congr - часть стандартной библиотеки или около того.
g1 = if x > -300 then f x else x
Не скомпилируется потому что не найдёт доказателство что x > -273.5.
Исходная версия AndreyKl, :
Как то так (в фигурных скобках неявный параметр, он должен выводиться из контекста).
gt_trans : {z : double} (x : double) -> (prf : x > y) -> (y > z) -> (x > z)
gt_dec : (x y : double) -> Either (x > y) (x <= y)
f : (x : Double) -> (prf : x > -273.5) -> Double
g x = if gt_dec x -50 == Left prf
then
f x (gt_trans x prf)
else
x
Функции вроде gt_trans , congr - часть стандартной библиотеки или около того.