agda

1열

1답변

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

내가 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 _ =

agda 2017-12-17

---

2열

2답변

표현이 평가되지 않음

지연 생성자가없는 CoList을 정의하려고합니다. with 표현식을 사용하지만 agda가 하위 케이스의 유형을 수정하지 않는 문제가 발생했습니다. module Failing where open import Data.Unit open import Data.Empty open import Data.Maybe open import Data.Nat op

agda dependent-type 2017-12-23

---

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를 사용하고 있습니다.

emacs agda agda-mode 2017-11-06

---

1열

1답변

Agda의 하스켈 (Haskell) 타입 안경이 왜 'Raw'로 시작 되는가? AGDA 표준 라이브러리에서

, 우리는 RawMonad가, RawApplicative는 등 RawMonad : ∀ {f} → (Set f → Set f) → Set _ RawMonad M = RawIMonad {I = ⊤} (λ _ _ → M) RawMonadZero : ∀ {f} → (Set f → Set f) → Set _ RawMonadZero M = RawIMonadZe

agda 2017-11-08

---

0열

1답변

`replace`를 통해 이러한 commutativity의 증명을 완성하는 방법은 무엇입니까?

this 설명서에는 증명을 완료하는 데 replace을 사용할 수있는 방법이 나와 있지만 rewrite으로 끝나며 이는 replace이라고 쓰는 구문 설탕처럼 보입니다. 나는 그것을 명시 적으로 사용하는 방법을 이해하는데 관심이있다. 정확하게 이해하면 S k = S (plus k 0)을 S (plus k 0) = S (plus k 0)으로 다시 쓸 수 있으

functional-programming proof agda idris 2017-12-31

---

2열

3답변

Agda의`Vec`에 안전한`length` 함수를 쓰는 방법은 무엇입니까?

Data.Vec이 (가) 있으므로 Vec은 무엇인지 알고 있습니다. Nat와 Vec이 동형임을 증명하고 싶습니다. 내가 성공적으로 냇가 VEC로 변환 할 수 있습니다 증명하는 함수를 만들었습니다 : I는 해당 vec→ℕ을 쓰기 위해 노력하고있어 ℕ→vec : (n : ℕ) → Vec ⊤ n ℕ→vec zero = [] ℕ→vec (suc a) = tt

agda dependent-type 2017-11-12

---

-1열

1답변

Agda에서 레코드/데이터 형식 안에 함수를 저장하려면 어떻게해야합니까?

문서를 읽었습니다. 그것은 말한다 : 엄격한 양성 조건은 data Bad : Set where bad : (Bad → Bad) → Bad -- A B C -- A is in a negative position, B and C are OK 생성자의 인자의 종류에 나쁜의 음의 발생이 있기 때문에 같은 선언을 배제한다. (Ba

function agda 2017-11-16

---

2열

1답변

단락이 모나드 계산에 "재미"의 경우

이 같은 Data.Maybe.monad을 사용하는 기능이 있습니다 유사한 typeCheck ν (f · e) = typeCheck ν e >>= λ { (u , e′) → typeCheck ν f >>= λ { (u′ ▷ t , f′) → u !≡ₜ u′ >>= λ { refl → pure (, (f′ · e′)) };

syntax pattern-matching monads agda 2017-11-19

---

1열

1답변

Agda의 유형 구분에서 별칭을 정의하는 방법은 무엇입니까?

내 코드 : 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

functional-programming agda 2017-11-20

---

2열

1답변

등식 추론 연산자는 실제로 어떻게 사용됩니까?

Agda Standard Library은 종이에서하는 것과 유사한 방식으로 교정본을 작성할 수있는 일부 운영자를 내보내거나 하스켈 지역 사회에서 어떻게 가르쳐 지는지 보여줍니다. 당신은 with 추상화, rewrite 또는 헬퍼 보조를 사용하여 목표를 정제함으로써 다소 체계적인 방식으로 "기존"Agda 증명을 쓸 수 있지만, 평등 추론 기본 요소를 사용하는

agda 2017-12-05

---