부조리 패턴을 예상 할 때 패턴 생성을 위해 agda2-mode를 사용하려면 어떻게해야합니까?</p> <pre><code>data _+_≡_ : ℕ → ℕ → ℕ → Set where znn : ∀ {n} → zero + n ≡ n sns : ∀ {m n k} → m + n ≡ k → suc m + n ≡ suc k </code></pre> <p>을 그리고 수동으로 증명할 수있다 : 예를 들어

Question

, 우리는 2 + 2 != 5을 증명하고

2+2≠5 : 2 + 2 ≡ 5 → ⊥ 
2+2≠5 (sns (sns())) 

을하지만 패턴 (sns (sns()))가 (단지 구멍을 채우는 등) 생성하고 싶습니다. 그것을 성취 할 수있는 방법이 있습니까?

나는 agda2 모드에서 Emacs 25를 사용하고 있습니다.

Answer 1

좋아, 그래서이 구성에서 시작 가정 해 봅시다 : 당신이 사용할 수있는이 경우

2+2≠5 : 2 + 2 ≡ 5 → ⊥ 
2+2≠5 h = {!!} 

를 이맥스 'keyboard macrosh에 일치에 의해 생성 된 하위 용어는 h을 지정됩니다 때문이다. 그래서 사용 :

• <f3>는
• C-c C-f (구멍으로 이동)
• C-c C-c h RET (h에 일치)
• <f4> (기록 매크로)

(매크로 기록을 시작합니다) 당신은 "첫 번째 목표 인 h와 일치하는 동작으로 이동"이라는 동작을 기록했습니다. 부조리 한 사례가 발생할 때까지 <f4>을 계속 누를 수 있습니다.