agda

1зной

1ответ

Я пытаюсь увидеть, как разветвиться на «безопасный» код. Например, ниже предлагается вызвать tail только на безопасном пути - то есть, если список на входе не пуст. Там будет простой способ, конечно,

1зной

1ответ

Agda: соответствие шаблону равным переменным?

Как опыт обучения, я пытаюсь реализовать проверенный регулярный выражетель, используя стиль продолжения прохождения в Agda, на основе предложенного в this paper. У меня есть тип регулярных выражений о

2зной

1ответ

Сохранение положительности функтора при переходе через продукт по отношению к вектору

В следующем коде определение А123 принимает μ₁, что имеет смысл. Если я свяжу узел с продуктом, как в μ₂, он по-прежнему принимается. Однако, если я попытаюсь пройти через вектор, как в μ₃, он больше

0зной

1ответ

Как написать эквивалентный код agda этого кода coq?

Я хочу написать данный код coq в agda. Definition included (D1 D2:R -> Prop) : Prop := forall x:R, D1 x -> D2 x. Я попытался таким образом .. data included (D1 D2 : R -> Set) : Set where foral

0зной

1ответ

Как это записать в agda?

Я хотел реализовать это утверждение в agda; A dedekind cut is a pair (L, U) of mere predicates L : Q -> Set and R : Q -> Set which is 1) inhibited : exists (q : Q) . L(q)^exists (r : Q) . U(r) Я по