AZ
с рынком у тебя есть венчурное инвестирование, где люди предлагают безумные идеи и некоторые реализуются, без него у тебя "НИИ Инновацинных технологий" который ничего полезного реально никогда не сделает
Size: a a a
2020 July 18
Rn
но в целом всё просто. get_number_from_user() - это пораждение уникального значения. add - это признак x + 1 - это можно выразить.
Rn
т.е. основная проблема в С++ когда-то была(и отчасти есть) - это первое
Rn
Rn
всё остальное - примитивно.
p
твоё недоязычок не может в это. Ты его переоцениваешь. Но сейчас я поищу - я когда-то писал подобное - мне лень искать
add1: (n: Int) -> S n
add1 n = n + 1
assert: (n1: Int) -> (n2: Int) -> {auto: n1 GTE n2} -> ()assert _ _ = ()
foo: IO ()
foo = do
a <- get_number
let a2 = add1 a
assert a1 a2
assert a2 a1 // error
pure ()
Вот на "недоязыке" (@psilon я правильно поуф записал?)
AZ
Сюда кто-то пришел скриптуху с двумя плюсами продавать? лол
AZ
add1: (n: Int) -> S n
add1 n = n + 1
assert: (n1: Int) -> (n2: Int) -> {auto: n1 GTE n2} -> ()assert _ _ = ()
foo: IO ()
foo = do
a <- get_number
let a2 = add1 a
assert a1 a2
assert a2 a1 // error
pure ()
Вот на "недоязыке" (@psilon я правильно поуф записал?)
нет, сравнение возвращает бул а тебе нужен DEC, для этого
{auto : n1 `GTE` n2}p
Там нет add1 функции
H
add1: (n: Int) -> S n
add1 n = n + 1
assert: (n1: Int) -> (n2: Int) -> {auto: n1 GTE n2} -> ()assert _ _ = ()
foo: IO ()
foo = do
a <- get_number
let a2 = add1 a
assert a1 a2
assert a2 a1 // error
pure ()
Вот на "недоязыке" (@psilon я правильно поуф записал?)
Функция
add1 не скомпилируетсяAZ
add1: (n: Int) -> S n
add1 n = n + 1
assert: (n1: Int) -> (n2: Int) -> {auto: n1 GTE n2} -> ()assert _ _ = ()
foo: IO ()
foo = do
a <- get_number
let a2 = add1 a
assert a1 a2
assert a2 a1 // error
pure ()
Вот на "недоязыке" (@psilon я правильно поуф записал?)
S n это не тип
Rn
Там нет add1 функции
Тебе сообщили, что это примтивная херня. К тому же, то что ты высрал - убожество бездарное и никак не сходится с тем, что ты показывал.
p
Стоп, это тот самый царь?
p
Тебе сообщили, что это примтивная херня. К тому же, то что ты высрал - убожество бездарное и никак не сходится с тем, что ты показывал.
Если примитивная то реализуй
Rn
тебе описали как она должна работать. Я жду возражений. Я не обязан предъявлять большие пруфы пока ты не ничего не можешь сделать более слабым
Rn
Если примитивная то реализуй
ответил выше. К тому же я не вижу ответа. Кукарекал одной, высрал мусор, да ещё и обделался
p
тебе описали как она должна работать. Я жду возражений. Я не обязан предъявлять большие пруфы пока ты не ничего не можешь сделать более слабым
Я описал тебе принцип работы сигнатурой
p
Ок, опишу словами
p
Функция add1 принимает число n, и возвращает число на 1 больше чем n
p
Все ясно в постановке задачи?