Зависимое сопоставление с образцом на x позволяет нам, учитывая реализацию P(...) для каждого возможного значения x в соответствующем случае, доказать P(x).Например:
λ (P : *)
λ (T : P True)
λ (F : P False)
λ (b : Bool)
case b as x returns P(x)
True => T
False => F
Здесь компилятор ожидает P(True) в первой ветви, P(False) во второй, и тогда все выражение будет иметь тип P(b).Таким образом, мое case b as x returns P ... выражение теоретически должно заменить сопоставление с образцом Агды.Но это не так: соответствие Агды также дает вам информацию о предыдущих аргументах.
foo : (b : Bool) -> IsTrue b -> ...
foo .true ItIsTrue = ...
Здесь сопоставление с образцом на IsTrue b сгенерировало информацию, которую b = true, что позволяет нам пропустить образец b = false.Это не было включено в мой синтаксис. Как именно Агда справляется с этой дополнительной информацией, и когда она знает, что из-за этого мы можем избежать паттерна?Возможно ли расширить мой атомарный синтаксис case of таким образом, чтобы это выполнялось так же, как это делает зависимое сопоставление с образцом Агды?