내가 AGDA의 특정 생성자에 대해 이야기하려면 어떻게

Question

내가

data Maybe : Set -> Set where 
    Just : forall {A} -> A -> Maybe A 
    Nothing : forall {A} -> Maybe A 

이 말하고, 나는

minus : Nat -> Nat -> Maybe Nat 
minus zero zero  = Just zero 
minus zero _   = Nothing 
minus n zero   = Just n 
minus (suc n) (suc m) = minus n m 

처럼 내 자신의 마이너스를 정의하고 내가 백만 FORALL 것을 증명하고 싶습니다 m 경우> n (마이너스 mn)은 항상 (Just Nat)을 울립니다. 이 유형을 어떻게 유형화 할 수 있는지 궁금합니다.

감사합니다.

Answer 1

표준 라이브러리의 Is-just을 사용할 수 있습니다. 성명은 다음과 같습니다 :

lt-minus-total : ∀ n m → m < n → Is-just (minus n m)