в языке есть равенство то там могут быть строки вида "A = B", а если есть ещё и константы то и "A = 0".
Но приведённое
A⊢B =0
это не предложение языка, и вообще бессмысленно, потому что само
A⊢B уже тоже не предложение языка.
Поэтому непонятно что значило бы что оно равно нулю. Что именно равно нулю то?
Нет. Она является конструктором индуктивного типа, если Вы знаете, что это такое. Если не знаете — просто частью синтаксиса, как тире и запятая в этом предложении.
Александр, а что это такое и где об этом можно прочитать? Я имею ввиду "конструктор индуктивного типа" и подобное. Изучаю логику, первый раз вижу эти термины.
это теория типов
Спасибо!
Обсуждают сегодня