Sabit bir aralık içinde Nat bakımı

Question

Sabit bir aralıkta kalan bir Nat kullanmak istiyorum. Numarayı menzil dışına iteceklerse başarısız olan incr ve işlevlerini isterim. Bu, Fin için iyi bir kullanım durumu gibi görünüyor, ama nasıl çalışacağından emin değilim.

- Returns the next value in the ordered finite set. 
- Returns Nothing if the input element is the last element in the set. 
incr : Fin n -> Maybe (Fin n) 

- Returns the previous value in the ordered finite set. 
- Returns Nothing if the input element is the first element in the set. 
decr : Fin n -> Maybe (Fin n) 

Nat bir Vect n içine endekse kullanılacaktır: tip imzaları bu gibi görünebilir. incr ve 'u nasıl uygularım? Bunun için Fin doğru seçim mi?

incr, decr : {n : Nat} -> Fin n -> Maybe (Fin n) 
incr {n=n} f = natToFin (succ $ finToNat f) n 

decr {n=n} f = case finToNat f of 
    Z => Nothing 
    S k => natToFin k n 

Answer 1

Ben kolay yolu Data.Fin bazı standart Fin↔Nat dönüşüm fonksiyonlarını kullanmaktır tahmin Coq standart kütüphanesi, vektörlere endeksleme için 'Fin'i kullanır. `Nth` işlevinin tanımına bakın (burada) (https://coq.inria.fr/library/Coq.Vectors.VectorDef.html).