С-абстракция и равенство - PullRequest
0 голосов
/ 15 мая 2019

В следующем примере

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

postulate
  f : Nat → Nat
  g : ∀{x y} → f x ≡ suc y → Nat

h : Nat → Nat
h x with f x
h x | zero = zero
h x | suc y = g {x} {y} {!refl!}

Agda не принимает refl в качестве аргумента.

Основные вопросы:

  1. что я делаю не так?
  2. каков правильный / оптимальный / установленный / предпочтительный способ доказательства подобных вещей?

И, конечно, мы очень ценим любое понимание поведения Агды.

1 Ответ

1 голос
/ 15 мая 2019

≡-Reasoning и 'with' pattern и Agda: тип не упрощен в with блок должен ответить на ваши вопросы. Официальные документы описывают, как делать то, что вы хотите, но они не слишком удобны для начинающих.

...