Agdaのタイプ解除でエイリアスを定義する方法は？

Question

マイコード：

law : ∀ a x → ((suc a) * (suc a) ÷ (suc a) ⟨ x ⟩) →ℕ ≡ (suc a , refl) 
law a x = refl 

（このコードはちょうど私の考えを説明し、それがコンパイルされません）私はあまりにも多くのsuc aがあると思うと、私は、suc aにのようなものを別名を与えたい：

law : ∀ a x → ((s : suc a) * s ÷ s ⟨ x ⟩) →ℕ ≡ (s , refl) 
law a x = refl 

これを達成できますか？

Answer 1

あなたはlet

law : ∀ a x → let s = suc a in (s * s ÷ s ⟨ x ⟩) →ℕ ≡ (s , refl) 
law a x = refl 

を使用するか、または匿名のモジュールを定義することができます。モジュールlawの外

module _ (a : ℕ) where 
    s = suc a 
    law : ∀ x → (s * s ÷ s ⟨ x ⟩) →ℕ ≡ (s , refl) 
    law x = refl 

は、あなたが提供するものと同じタイプの署名を持っています。