एक निश्चित सीमा के भीतर एक नाट को बनाए रखना

Question

मुझे Nat होना चाहिए जो एक निश्चित सीमा के भीतर रहता है। मैं incr और decr फ़ंक्शंस करना चाहता हूं जो विफल हो जाते हैं यदि वे सीमा के बाहर संख्या को धक्का दे रहे हैं। ऐसा लगता है कि यह Fin के लिए एक अच्छा उपयोग केस हो सकता है, लेकिन मुझे सच में यकीन नहीं है कि इसे कैसे काम करना है।

- 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 एक Vect n में सूचकांक के लिए उपयोग किया जाएगा: प्रकार हस्ताक्षर कुछ इस तरह लग सकता है। मैं incr और decr कैसे कार्यान्वित कर सकता हूं? Fin भी इसके लिए सही विकल्प है?

Answer 1

मुझे लगता है कि सबसे आसान तरीका है Data.Fin से कुछ मानक Fin↔Nat रूपांतरण कार्यों का उपयोग करने के लिए है:

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