时间戳

首页 > 解决方案 > Agda：重写子表达式

agda - Agda：重写子表达式

问题描述

我试图证明：

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

出现了。

我不确定如何解决这个问题。从这里我明白这与隐含的论点有关。但不确定如何解决

这种错误表示未解决的元变量，这意味着 Agda 无法推断出隐式参数

谢谢！

标签： agda

解决方案

您不A使用AddTodoSetsNewCompletedToFalse. 此外，这不是错误，而是未解决的元数据。

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

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

推荐阅读