问题描述
我正在尝试定义一个简单的谓词，以确定一个公式是否是通过简单的归纳定义语法定义的给定形式的子公式。我遇到了一些可能很简单的问题。
（i）我宁愿使用具有给定类型A的参数化模块。就A具有可决定的相等性而言，如何导入A是集合的信息？如果无法完成，有什么解决方法？这就是为什么我有Nat的原因。
（ii）
from drf_yasg.inspectors import PaginatorInspector
from drf_yasg import openapi
class LimitOffsetPaginatorInspectorClass(PaginatorInspector):
def get_paginated_response(self,paginator,response_schema):
"""
:param BasePagination paginator: the paginator
:param openapi.Schema response_schema: the response schema that must be paged.
:rtype: openapi.Schema
"""
return openapi.Schema(
type=openapi.TYPE_OBJECT,properties=OrderedDict((
('count',openapi.Schema(type=openapi.TYPE_INTEGER)),('next',openapi.Schema(
type=openapi.TYPE_OBJECT,properties=OrderedDict((
('offset',('limit',openapi.Schema(type=openapi.TYPE_INTEGER))
))
)),('results',response_schema),)),required=['results']
)
def get_paginator_parameters(self,paginator):
"""
Get the pagination parameters for a single paginator **instance**.
Should return :data:`.NotHandled` if this inspector does not kNow how to handle the given `paginator`.
:param BasePagination paginator: the paginator
:rtype: list[openapi.Parameter]
"""
return [
openapi.Parameter('offset',openapi.IN_QUERY,"Offset for Pagination",False,None,openapi.TYPE_INTEGER),openapi.Parameter('limit',"Page Size",openapi.TYPE_INTEGER)
]```
（和类似定义）谓词t1 ≡ (t2 // t3)是处理相等子公式的正确方法吗？如果不是，那么如何轻松地做到这一点？我还考虑过为isSubFormula编写一个谓词，然后使用equalFmla来创建一个全局子公式谓词，但是不确定这是否干净。
（iii）当我在第一行的内部进行图案匹配时，为什么最后三行会突出显示蓝色？我该如何解决
（iv）为什么isSubFormula ⊎ equalFmla不能在下面进行细化？
{!Data.Nat._≟_ n1 n2 !}解决方法
有很多不同的问题；如果您分别发布每个问题，则Stack Overflow效果更好。
不过，这里有一些答案：
（i）我宁愿使用具有给定类型A的参数化模块。 从A具有的意义上讲，一个导入A是集合的信息 可决定的平等？
您可以通过决策程序对模块进行参数设置，即类似这样的内容：
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
module categorical1 {A : Set} (_≟_ : Decidable (_≡_ {A = A})) where
请注意，我们在模块标头之前导入了Relation.Binary（用于Decidable）和R.B.PropositionalEquality（用于_≡_），因为参数类型我们模块的功能取决于这些定义。
（iii）为什么我进行模式匹配时后三行会突出显示蓝色 内部的第一个？我该如何解决
这是阿格达（Agda）警告您，这些子句在定义上将不成立，因为它们取决于与t1不匹配的先前子句。
（iv）为什么{！Data.Nat。≟ n1 n2！}在下面进行细化？
因为isSubFormula返回了Set，但是n1 ≟ n2返回了Dec _≡_。
我认为您的代码中对于isSubFormula是命题还是决策程序感到困惑。如果返回Set，则表示这是一个命题。您可以这样写，没有可判定的相等性，因为没有什么可决定的-两个isSubFormula的{{1}}值表示它们相等：
base如果需要决策程序，则可以通过写isSubFormula : tSymb → tSymb → Set
isSubFormula (base n1) (base n2) = n1 ≡ n2
或保留isSubFormula : tSymb → tSymb → Bool作为命题并编写isSubFormula来做到“布尔盲”操作。
请注意，如果您要决定decSubFormula : Decidable isSubFormula，则只需要A上具有可判定的相等性，便可以这样做
isSubFormula