Это дескридитация преподавательского состава и университета прежде всего

Я бы мог сделать, но мне студентов больше жаль, чем зларадствовать над ними лучше помочь

А оптимизации на AST делают, просто это дорогой подход

Да никакой, это и делают иногда специальные оптимизации для языков, обычно это выносят в ssa или mlir потому что во-первых так проще во вторых можно шарить между языками

Тоесть допустим вы пишете модуль для покрытия матчинга, он доступен теперь для всех фронтов что как то могут затранслировать паттерн

ржу

А не получится вспомнить какие-то специфичные оптимизации, например такое переписывание программы, которое не выразимо в языке, который парсят?

Например, джампы какие-нибудь.

Раз уж тут много людей из логики, вопрос. Вот есть кванторы, работают они примерно как if:

∀(условие) {тело}

Но математики не могут в однозначно интерпретируемые грамматики, так что обычно пишут просто

∀условие тело

(иногда одно либо другое оборачивают в скобки)

Однако мой препод с Физтеха писал

∀условие → тело
∃условие : тело

И это kind of имело смысл. Стрелка читается как "верно, что", а двоеточие как "такой, что", и при отрицании ∀ меняется на ∃, а → меняется на :

Интересно узнать, может кто-то встречал подобную или ещё какую-то альтернативную запись?

P.S. лекции Петровича теперь есть на ютубе, я посмотрел, и он obviously перестал так писать, теперь пишет через пробелы, как и все остальные

Лучшее, что сейчас есть — это вот этот вот ад со скобочками

ping @amaka_hahina

в типотеоретических пруверах обычно или явно пишут forall/exists, или используют сигнатуру зависимых функций для всеобщности, а для существования какой то сахар на тему сигмы или **

Кванторы применяются к переменным, а не к условиям. В некоторых синтаксисах они просто декорируют переменную (например, в условии), в некоторых вводятся отдельно.

Ну ок, $квантор($переменная|$условия) {$тело}

Пишу на суржике из математических конструкций и программерских

условие это часть тела в таком случае

Не так. Обычно что-то из:
1. (exists x) > 0
2. exists x (x > 0)

для существования второй вариант, да