Преобразовать индексированный тип данных Agda в запись - PullRequest
Новая
       12

Преобразовать индексированный тип данных Agda в запись

0 голосов
/ 07 октября 2019

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

record Foo : Set where
    fields
        x : Nat
        y : Nat
        z : Nat

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

data IsValidFoo : Foo → Set where
    validFoo : (foo : Foo) → Even (Foo.x foo) → (Foo.y foo) < (Foo.z foo) → IsValidFoo foo

validateFoo : (foo : Foo) → Maybe (IsValidFoo foo)
…

Я хочу иметь возможность получить доступ к отдельным доказательствам в IsValidFoo по имени и мысли о преобразовании IsValidFoo в тип записи. Возможно ли это и как этого достичь, если я хочу, чтобы его тип оставался IsValidFoo : Foo → Set?

1 Ответ

4 голосов
/ 07 октября 2019

Конечно, это возможно, определив IsValidFoo как тип записи, параметризованный по foo : Foo: 

open import Agda.Builtin.Nat hiding (_<_)

postulate
  _<_ : Nat → Nat → Set
  Even : Nat → Set
  Maybe : Set → Set

record Foo : Set where
  field
    x : Nat
    y : Nat
    z : Nat

record IsValidFoo (foo : Foo) : Set where
  constructor validFoo
  field
    even-x : Even (Foo.x foo)
    y<z    : (Foo.y foo) < (Foo.z foo)

validateFoo : (foo : Foo) → Maybe (IsValidFoo foo)
...