Evidence¶
Kernel-generated equality evidence.
Kernel-generated equality evidence.
The first QIEC kernel has no arbitrary user proof language. Evidence is either reflexivity or a rigid branch given introduced by GADT elimination.
EqualityEvidence = Reflexivity | BranchGiven
Kernel-generated evidence of a static equality: reflexivity or a branch's given.
dataclass
¶
Reflexivity(equality: EqualityType, tag: Literal['reflexivity'] = 'reflexivity')
Evidence that an equality holds because both sides are the same term.
| PARAMETER | DESCRIPTION |
|---|---|
equality
|
The proposition witnessed, whose sides must be equal.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
dataclass
¶
BranchGiven(id: EqualityId, equality: EqualityType, tag: Literal['branch_given'] = 'branch_given')
Evidence granted by a case branch's constructor refinement.
| PARAMETER | DESCRIPTION |
|---|---|
id
|
The stable identity of the given, derived from the branch scope.
TYPE:
|
equality
|
The proposition the branch's constructor makes available.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|