Agda 未解决的元数据

Question

我创建了一个树数据类型。以及一个应该从中检索值的 get 函数。我现在想创建一个证明，从空树中检索任何值都将返回“无”。

（我发出了 get' 和 Tree' 定义，因为我认为它们不相关。如果需要它们，我将包含它们）

    data Tree (A : Set) : Set where 
        Empty : Tree A
        Nodes : Tree' A -> Tree A 

    get : {A : Set} -> Positive -> Tree A -> Maybe A
    get _ Empty = nothing
    get p (Nodes n) = get' p n

    data Positive : Set where 
        xH : Positive
        xI : Positive -> Positive
        xO : Positive -> Positive

gempty : (p : Positive) -> get p Tree.Empty ≡ nothing
gempty p = refl

使用“agda ./proofs.agda”运行此代码我总是遇到

Unsolved metas at the following locations:
  .../src/proofs.agda:12,28-31

指向 gempty 的

get

。

因为我在项目的其他部分使用了 get 函数，所以我可以使用它，假设问题直接在证明声明中。

但是，我是Agda新手，不知道如何解决这个问题。如果您能指出正确的方向来解决我的问题，我将不胜感激。

编辑：最小示例

open import Data.Maybe
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app)
open Eq.≡-Reasoning

data Tree' (A : Set) : Set where 
        node001 : Tree' A -> Tree' A

data Tree (A : Set) : Set where 
        Empty : Tree A
        Nodes : Tree' A -> Tree A 

data Positive : Set where 
    xH : Positive
    xI : Positive -> Positive
    xO : Positive -> Positive

get' : {A : Set} -> Positive -> Tree' A -> Maybe A 
get' xH (node001 _ ) = nothing
get' (xO q) (node001 _ )= nothing
get' (xI q) (node001 r )= get' q r

get : {A : Set} -> Positive -> Tree A -> Maybe A
get _ Empty = nothing
get p (Nodes n) = get' p n


gempty : {A : Set} -> ∀ (p : Positive) -> get p Tree.Empty ≡ nothing
gempty p = refl

Answer 1

Agda 告诉你未解决的元是：

_A_27 : Set

即它不知道

A

的应用中

get

是什么类型。这是有道理的，因为

Tree.Empty

可以是任何类型的树。因此，您必须显式地传递在类型开头声明的类型

A

，对于

{A}

中的

get

参数或

{A}

中的

Tree.Empty

参数。

因此，以下任一工作：

gempty : {A : Set} -> ∀ (p : Positive) -> get {A = A} p Tree.Empty ≡ nothing

或

gempty : {A : Set} -> ∀ (p : Positive) -> get p (Tree.Empty {A = A}) ≡ nothing