несовместимость вселенной с сумбулом - PullRequest
Новая
       15

несовместимость вселенной с сумбулом

1 голос
/ 12 апреля 2019

Я определил и доказал следующую лемму: 

    NM.In k m -> {NM.In k m0}+{NM.In k m1}.

Я также могу доказать симметричную лемму для: 

    {NM.In k m0}+{NM.In k m1} -> NM.In k m

Однако, когда я пытаюсь объединить их в одну как:

    NM.In k m <-> {NM.In k m0}+{NM.In k m1}.

Я получил следующую ошибку: 

The term "sumbool (@NM.In CarrierA k m0) (@NM.In CarrierA k m1)" has type 
"Set" while it is expected to have type "Prop" (universe inconsistency: Cannot enforce
Set = Prop).

Как это можно решить?

1 Ответ

1 голос
/ 12 апреля 2019

Как отметил Даниэль, проблема в том, что связное <-> принимает в качестве аргументов только суждения, а sumbool живет в Set. Это может быть обойдено несколькими способами: вы можете заменить sumbool на or, или вы можете заменить iff на вычислительно релевантное соединение: 

Variables A B C : Prop.

Check (({A} + {B} -> C) * (C -> {A} + {B}))%type.
...