agda-mode

1열

1답변

나는 agda를 배우고 더 나은 이해를 얻기 위해 목록에 연습하고있다. 지금은 목록에 함수를 작성하려고합니다. 빈 목록의 머리와 꼬리를 반환하는 방법에 대해 혼란 스럽습니다. data list (A : Set) : Set where [] : list A _∷_ : A → list A → list A Null : {A : Set} → (list A)

3열

1답변

Agda : 스택과 함께 설치할 때 std-lib를 찾을 수 없습니다.

Agda 파일을 컴파일하려고하는데 표준 라이브러리를 찾는 데 문제가 있습니다. 문서 here을 보았습니다. 나는 그것을 설치하는 스택을 사용했습니다 : > which agda /home/joey/.local/bin/agda 을 그리고 난 내 AGDA 디렉토리를 환경 변수를 설정 한 : 올바른 파일로 채워집니다 > echo $AGDA_DIR /home

2열

1답변

부조리 패턴을 예상 할 때 패턴 생성을 위해 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>을 그리고 수동으로 증명할 수있다 : 예를 들어

, 우리는 2 + 2 != 5을 증명하고 2+2≠5 : 2 + 2 ≡ 5 → ⊥ 2+2≠5 (sns (sns())) 을하지만 패턴 (sns (sns()))가 (단지 구멍을 채우는 등) 생성하고 싶습니다. 그것을 성취 할 수있는 방법이 있습니까? 나는 agda2 모드에서 Emacs 25를 사용하고 있습니다.