G
Size: a a a
2020 March 25
AZ
ну у тебя x откуда взялся?
G
bar : (x > 500 = False) -> Int
bar prf = 1
Так скомпилировалось
G
Это то, что я хотел
AZ
твоя запись для меня бессмысленна
AZ
ты говоришь что какой-то x больше 500 хотя x даже не объявлен
p
то есть ввод там вообще не предусмотрен? Или я должен знать и доказать, что пользователь введет?
Предусмотрен
p
Ты должен доказать что функция вызовется только на данных указанных в пруфе
G
ты говоришь что какой-то x больше 500 хотя x даже не объявлен
Хорошо,
bar : x -> (x > 500 = False) -> Int
S
конкретная ситуация - пользователь вводит с консоли два числа, программа их должна суммировать, а функция суммирования принимает два аргумента с типом, в который входят целые числа от двух до пяти
p
Самый простой пример: банальный иф
p
Внутрь зайдет программа при выполнении условия
S
Ты должен доказать что функция вызовется только на данных указанных в пруфе
А это как доказать? И кому?
G
конкретная ситуация - пользователь вводит с консоли два числа, программа их должна суммировать, а функция суммирования принимает два аргумента с типом, в который входят целые числа от двух до пяти
G
Ввод пользователя тоже
AZ
Хорошо,
bar : x -> (x > 500 = False) -> Int
ну и вызываешь:
if (x > 500 = False) (bar x Refl) 10p
А это как доказать? И кому?
То есть
x: i32 = read()
if x > 10 {
bar(x)
}
Здесь x внутри тела ИФА будет иметь тип x: i32{x>10}
x: i32 = read()
if x > 10 {
bar(x)
}
Здесь x внутри тела ИФА будет иметь тип x: i32{x>10}
S
То есть
x: i32 = read()
if x > 10 {
bar(x)
}
Здесь x внутри тела ИФА будет иметь тип x: i32{x>10}
x: i32 = read()
if x > 10 {
bar(x)
}
Здесь x внутри тела ИФА будет иметь тип x: i32{x>10}
А если ввести text?
p
А если ввести text?
Я тебе на псевдокоде привел
p
В реальности тебе нужно доказать что там будет число, да