Agda：重写子表达式

Question

我想证明：

AddTodoSetsNewCompletedToFalse :
  ∀ {n : ℕ} (todos : Vec Todo (1 + n)) (text : String) →
    Todo.completed (last (AddTodo todos text)) ≡ false
AddTodoSetsNewCompletedToFalse todos text = ?

哪里

AddTodoLastAddedElementIsTodo :
  ∀ {a} {A : Set a} {n} (todos : Vec Todo n) (text : String) →
    last (AddTodo todos text) ≡ 
      record
        { id        = 1
        ; completed = false
        ; text      = text
        }
AddTodoLastAddedElementIsTodo todos text = vecLast todos

和

vecLast : ∀ {a} {A : Set a} {l n} (xs : Vec A n) → last (xs ∷ʳ l) ≡ l
vecLast []       = refl
vecLast (_ ∷ xs) = P.trans (prop (xs ∷ʳ _)) (vecLast xs)
  where
    prop : ∀ {a} {A : Set a} {n x} (xs : Vec A (suc n)) → last (x ∷ xs) ≡ last xs
    prop xs with initLast xs
    ...        | _ , _ , refl = refl

我尝试使用 rewrite 并得到：

AddTodoSetsNewCompletedToFalse :
  ∀ {a} {A : Set a} {n} (todos : Vec Todo n) (text : String) →
    Todo.completed (last (AddTodo todos text)) ≡ false
AddTodoSetsNewCompletedToFalse todos text rewrite AddTodoLastAddedElementIsTodo todos text = refl

但是错误：

_a_100 : Agda.Primitive.Level

出现了。

我不确定如何解决这个问题。来自我了解到这与隐式参数有关。但不确定如何修复它

This sort of error indicates an unsolved metavariable, which means that Agda has failed to infer an implicit argument

谢谢！

Answer 1

您不对 AddTodoSetsNewCompletedToFalse 类型的任何内容使用 A。另外，这不是错误，而是未解决的元数据。

所以发生的事情是，无论您在哪里使用 AddTodoSetsNewCompletedToFalse，参数或结果类型中都没有限制 A（以及随后的 a）的选择，因此统一器无法解决这些元变量。您可以通过编写 AddTodoSetsNewCompletedToFalse {a = _} {A = _} 并观察这两个元数据未解决来明确说明会发生什么。

您应该简单地从 AddTodoSetsNewCompletedToFalse 的类型中删除前两个参数（a 和 A）。

Agda：重写子表达式

Agda: rewrite subexpression

agda