Нет, все норм, просто компилятор шарпа умеет инлайнить только вызовы непосредственно метода, а если метод запаковали в делегат и передали как значение - не умеет. Впрочем, сам прием для сишарпа абсолютно несвойственнен и поэтому срочнаааа фиксить никто не побежит

окей, спасибо

Скорее всего потому, что такая нотация нигде в математике и не нужна.

дак и жадном языке можно лениво вычислять. Только зачем всегда вычислять лениво, если это лишний оверхед?

Так что каждый раз, когда ты захочешь использовать ? : в математике, тебе придётся определять данный оператор:

〚p? x : y〛 ≔ ιz(Ez : ((p → z = x) ∧ (¬p → z = y)))

для консистентных систем без возможно незначащих формул

А я вот не уверен

В случае Шарпа инлайнит даже не копилятор а Джит в рантайме. В фарше инлайнит компилятор

Луа как вариант

Возьмите Ocaml

#/usr/bin/ocaml

сверху и вперёд.

По-моему, в любом учебнике есть.

Артангенс с X около нуля.
Или ещё что-нибудь с разрывом в области определения функции.

В фигурных скобках, на нескольких строках.

Для параконсистентных сложнее. Использовать равенство будет некорректно, если равенство обладает свойством евклидовости. Мы должны либо переформулировать это вовсе, либо использовать альтернативное равенство, которое будет обозначать реляционную идентичность так, что оно будет неевклидовым, либо использовать тринитарную логику (внезапно). Иначе для 〚p ? 1 : 2〛 может получиться, что 1 = 2.

Переформулировать можно в том числе через замену конъюнкции на некоторый оператор, работающий в нужной семантике абстрактных ресурсов так, что не проверяется, что ¬p, если p.

Если не так, то мы получим сразу два значения z, и оператор определённой дескрипции здесь не работает, а сразу несколько значений нам при этом получать не нужно. Тогда можно использовать оператор множественной дескрипции, определить специальное значение ⊥ и возвращать его, если мощность получаемого множества равняется двум.

Также в любом случае нужно гарантировать, что такой Ez.P всегда выполняется

В консистентном случае на рефлексивных логиках со всегда значащими термами это элементарно, так как там используется самое типичное равенство, для которого верно, что a = a, определяй равенство или не определяй, и существует такой z как тот же 1 или 2, из чего можно показать, что такой z = 1 или 2

В нерефлексивных логиках определяемое равенство не может использоваться для доказательства a = a, последнее должно быть специально задано как свойство равенства.

Под рефлексивностью имею в виду наличие соответствующего структурного правила.

В логиках с возможно незначащими термами нужно определять поведение, когда x и/или y в x = y не имеют значения (не обозначают некоторый индивидуал)

В случае возможно незначащих (possible non-denoting) формул конструкцию нужно дополнить для p, не имеющего никакого значения, так как p и ¬p не описывают любое денотационное поведение p. Для языков программирования можно представить, что if-clause никогда не завершается, и здесь как раз случай non-denoting formula.

Конечно, использование так определённого тернарного оператора подразумевает, что в таком случае мы на уровне семантики знаем, что формула non-denoting...

Но в ЯП, если мы будем иметь никогда не завершающейся if-clause, то мы либо попросту не дойдём до использования оператора, так как на if-clause всё зависнет, либо заранее будем иметь синтаксическое доказательство, что if-clause никогда не будет вычислена, а наша формальная система будет такой, что от доказательства мы сможем перейти к требуемому pattern matching, да и само доказательство можно записать (это требует синтаксической версии "[this] is non-denoting formula")

Я все.