Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-11-05 07:05:32 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of github.com:kind-lang/kind

Browse Source
This commit is contained in:
MaiaVictor 2021-11-10 20:08:35 -03:00
commit 3525f7e0ca
1 changed files with 7 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
base/RLP/aux.kind
View File

@ -5,9 +5,14 @@
RLP.aux.0(
add: Nat
len: Nat
pf0: Either<Equal<Nat, add, 128>, Equal<Nat, add, 192>>
H0: Either<Equal<Nat, add, 128>, Equal<Nat, add, 192>>
): Nat.ltn(0,Nat.add(add,len)) == Bool.true
RLP.aux.0(add, len, pf0)
case H0 {
} default
case mirror(H0.value) {
refl:
refl
}: Nat.ltn(0,Nat.add(self.b,len)) == Bool.true
// TODO: include `a <= 192`
RLP.aux.1(