mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-11-05 07:05:32 +03:00
prove everything except two lemmas
This commit is contained in:
Rígille S. B. Menezes
parent
30003dd12c
commit
0d9f0dc30a
@ -29,7 +29,7 @@ RLP.aux.split.0(
|
||||
RLP.aux.split.1(
|
||||
payload: Bytes
|
||||
tail: Bytes
|
||||
H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
|
||||
H: Equal<Bool>(Nat.lte(List.length!(payload), 55), false)
|
||||
): Pair.new(Bytes, Bytes, payload, tail) ==
|
||||
let b = Bytes.from_nat(List.length!(payload))
|
||||
let a = Nat.to_u8(Nat.add(56, Nat.add(128, List.length!(b))))
|
||||
|
||||
@ -21,76 +21,84 @@ RLP.encode_identity(
|
||||
(bound.snd.fst, bound.snd.snd)
|
||||
case rlps.head with bound.snd.fst bound.snd.snd {
|
||||
data:
|
||||
because_i_said_so!
|
||||
// let conditions = Bool.and.split(Nat.eql(List.length!(rlps.head.value),1), Nat.lte(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 127))
|
||||
// def condition = Bool.and(Nat.eql(List.length!(rlps.head.value),1), Nat.lte(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 127))
|
||||
// case condition with conditions {
|
||||
// true:
|
||||
// case rlps.head.value with conditions {
|
||||
// cons:
|
||||
// case rlps.head.value.tail with conditions {
|
||||
// nil:
|
||||
// open conditions
|
||||
// let conditions.snd = mirror(conditions.snd)
|
||||
// case conditions.snd {
|
||||
// refl:
|
||||
// // data([rlps.head.value.head]) & RLP.decode.many(RLP.encode.many(rlps.tail)) == data([rlps.head.value.head]) & rlps.tail
|
||||
// let ind = RLP.encode_identity(rlps.tail, ?todo.8)
|
||||
// apply(List.cons(RLP, RLP.data([rlps.head.value.head])), ind)
|
||||
// }: conditions.snd.b( () List(RLP),List.cons(RLP,RLP.data(List.cons(U8,rlps.head.value.head,List.nil(U8))),RLP.decode.many(List.concat(U8,List.nil(U8),RLP.encode.many(rlps.tail)))),Nat.lte(U8.to_nat(rlps.head.value.head),191,() List(RLP),RLP.split.length(128,List.cons(U8,rlps.head.value.head,List.concat(U8,List.nil(U8),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,rlps.head.value.head,List.concat(U8,List.nil(U8),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.data(List.cons(U8,rlps.head.value.head,List.nil(U8))),rlps.tail)
|
||||
//
|
||||
// cons:
|
||||
// open conditions
|
||||
// Empty.absurd!(Bool.false_neq_true(conditions.fst))
|
||||
// }! :: RLP.decode.many(List.concat(U8,List.cons(U8,rlps.head.value.head,rlps.head.value.tail),RLP.encode.many(rlps.tail))) == List.cons(RLP,RLP.data(List.cons(U8,rlps.head.value.head,rlps.head.value.tail)),rlps.tail)
|
||||
// //?true-278
|
||||
// nil:
|
||||
// open conditions
|
||||
// Empty.absurd!(Bool.false_neq_true(conditions.fst))
|
||||
// }!
|
||||
// false:
|
||||
// //?false-278-10-2370-152742
|
||||
// case Nat.lte(List.length(U8,rlps.head.value),55) {
|
||||
// true:
|
||||
// let recover_prefix = ?todo.9 :: Nat.add(128, List.length(U8, rlps.head.value)) == U8.to_nat(Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))))
|
||||
// case recover_prefix {
|
||||
// refl:
|
||||
// let limit_size = ?todo.10 :: true == Nat.lte(List.length(U8,rlps.head.value), 63)
|
||||
// case limit_size {
|
||||
// refl:
|
||||
// let split_id = RLP.aux.split.0(rlps.head.value, RLP.encode.many(rlps.tail), ?todo.11)
|
||||
// case split_id {
|
||||
// refl:
|
||||
// let ind = RLP.encode_identity(rlps.tail, ?todo.12)
|
||||
// apply(List.cons(RLP,RLP.data(rlps.head.value)), ind)
|
||||
// }: split_id.b(() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
// }: limit_size.b(() List(RLP),RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.concat(U8,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
//
|
||||
// }: Nat.lte( recover_prefix.b ,127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8))),RLP.decode.many(List.concat(U8,List.concat(U8,List.nil(U8),rlps.head.value),RLP.encode.many(rlps.tail)))),Nat.lte( recover_prefix.b ,191,() List(RLP),RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.concat(U8,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
//
|
||||
//// ?true-4418-1090-258-258
|
||||
// false:
|
||||
// let recover_prefix = ?todo.13 :: Nat.add(184, List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))) == U8.to_nat(Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))))
|
||||
// case recover_prefix {
|
||||
// refl:
|
||||
// let limit_length = ?todo.14 :: true == Nat.lte(List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value))), 7)
|
||||
// case limit_length {
|
||||
// refl:
|
||||
// let recover_split = RLP.aux.split.1(rlps.head.value, RLP.encode.many(rlps.tail), ?todo.15)
|
||||
// case recover_split {
|
||||
// refl:
|
||||
// let ind = RLP.encode_identity(rlps.tail, ?todo.16)
|
||||
// apply(List.cons(RLP,RLP.data(rlps.head.value)), ind)
|
||||
// }: recover_split.b(() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
//
|
||||
// }: limit_length.b( () List(RLP),RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value))),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.concat(U8,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
//
|
||||
// }: Nat.lte( recover_prefix.b ,127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),List.nil(U8))),RLP.decode.many(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)))),Nat.lte( recover_prefix.b ,191,() List(RLP),RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value))),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.concat(U8,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
//
|
||||
// //?false-4418-1090-258-258
|
||||
// }: List.concat(U8,List.concat(U8, self( () Bytes,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value)))),rlps.head.value),RLP.encode.many(rlps.tail),(bytes) List(RLP),List.nil(RLP),(bytes.head) (bytes.tail) Nat.lte(U8.to_nat(bytes.head),127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,bytes.head,List.nil(U8))),RLP.decode.many(bytes.tail)),Nat.lte(U8.to_nat(bytes.head),191,() List(RLP),RLP.split.length(128,List.concat(U8,List.concat(U8, self( () Bytes,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value)))),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.concat(U8,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
//
|
||||
// }! :: RLP.decode.many(List.concat(U8, condition( () List(U8),rlps.head.value,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value)),RLP.encode.many(rlps.tail))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
let conditions = Bool.and.split(Nat.eql(List.length!(rlps.head.value),1), Nat.lte(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 127))
|
||||
def condition = Bool.and(Nat.eql(List.length!(rlps.head.value),1), Nat.lte(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 127))
|
||||
case condition with conditions {
|
||||
true:
|
||||
case rlps.head.value with conditions {
|
||||
cons:
|
||||
case rlps.head.value.tail with conditions {
|
||||
nil:
|
||||
open conditions
|
||||
let conditions.snd = mirror(conditions.snd)
|
||||
case conditions.snd {
|
||||
refl:
|
||||
// data([rlps.head.value.head]) & RLP.decode.many(RLP.encode.many(rlps.tail)) == data([rlps.head.value.head]) & rlps.tail
|
||||
open bound.snd.snd as bound_tail
|
||||
let ind = RLP.encode_identity(rlps.tail, bound_tail.fst)
|
||||
apply(List.cons(RLP, RLP.data([rlps.head.value.head])), ind)
|
||||
}: conditions.snd.b( () List(RLP),List.cons(RLP,RLP.data(List.cons(U8,rlps.head.value.head,List.nil(U8))),RLP.decode.many(List.concat(U8,List.nil(U8),RLP.encode.many(rlps.tail)))),Nat.lte(U8.to_nat(rlps.head.value.head),191,() List(RLP),RLP.split.length(128,List.cons(U8,rlps.head.value.head,List.concat(U8,List.nil(U8),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,rlps.head.value.head,List.concat(U8,List.nil(U8),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.data(List.cons(U8,rlps.head.value.head,List.nil(U8))),rlps.tail)
|
||||
|
||||
cons:
|
||||
open conditions
|
||||
Empty.absurd!(Bool.false_neq_true(conditions.fst))
|
||||
}! :: RLP.decode.many(List.concat(U8,List.cons(U8,rlps.head.value.head,rlps.head.value.tail),RLP.encode.many(rlps.tail))) == List.cons(RLP,RLP.data(List.cons(U8,rlps.head.value.head,rlps.head.value.tail)),rlps.tail)
|
||||
//?true-278
|
||||
nil:
|
||||
open conditions
|
||||
Empty.absurd!(Bool.false_neq_true(conditions.fst))
|
||||
}!
|
||||
false:
|
||||
//?false-278-10-2370-152742
|
||||
let size_limit = Equal.refl(Bool, Nat.lte(List.length(U8,rlps.head.value),55))
|
||||
case Nat.lte(List.length(U8,rlps.head.value),55)
|
||||
with size_limit: Equal(Bool, Nat.lte(List.length(U8,rlps.head.value),55), self) {
|
||||
true:
|
||||
let recover_prefix = Nat.to_u8.safe_conversion(Nat.add(128,List.length(U8,rlps.head.value))
|
||||
Nat.lte.slack_left(List.length(U8,rlps.head.value), 55, 72, size_limit))
|
||||
case recover_prefix {
|
||||
refl:
|
||||
let limit_size = mirror(Nat.lte.slack_left(List.length(U8,rlps.head.value),55, 8, size_limit))
|
||||
case limit_size {
|
||||
refl:
|
||||
let split_id = RLP.aux.split.0(rlps.head.value, RLP.encode.many(rlps.tail), size_limit)
|
||||
case split_id {
|
||||
refl:
|
||||
open bound.snd.snd as bound_tail
|
||||
let ind = RLP.encode_identity(rlps.tail, bound_tail.fst)
|
||||
apply(List.cons(RLP,RLP.data(rlps.head.value)), ind)
|
||||
}: split_id.b(() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
}: limit_size.b(() List(RLP),RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.concat(U8,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
|
||||
}: Nat.lte( recover_prefix.b ,127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8))),RLP.decode.many(List.concat(U8,List.concat(U8,List.nil(U8),rlps.head.value),RLP.encode.many(rlps.tail)))),Nat.lte( recover_prefix.b ,191,() List(RLP),RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.concat(U8,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
|
||||
// ?true-4418-1090-258-258
|
||||
false:
|
||||
let limit_size_length = RLP.aux.bytes_from_nat(List.length(U8,rlps.head.value), bound.snd.fst)
|
||||
let recover_prefix = Nat.to_u8.safe_conversion(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))
|
||||
Nat.lte.slack_left(List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value))), 7, 64, limit_size_length)
|
||||
)
|
||||
case recover_prefix {
|
||||
refl:
|
||||
let limit_length = mirror(RLP.aux.bytes_from_nat(List.length(U8,rlps.head.value), bound.snd.fst))
|
||||
case limit_length {
|
||||
refl:
|
||||
let recover_split = RLP.aux.split.1(rlps.head.value, RLP.encode.many(rlps.tail), size_limit)
|
||||
case recover_split {
|
||||
refl:
|
||||
open bound.snd.snd as bound_tail
|
||||
let ind = RLP.encode_identity(rlps.tail, bound_tail.fst)
|
||||
apply(List.cons(RLP,RLP.data(rlps.head.value)), ind)
|
||||
}: recover_split.b(() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
|
||||
}: limit_length.b( () List(RLP),RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value))),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.concat(U8,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
|
||||
}: Nat.lte( recover_prefix.b ,127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),List.nil(U8))),RLP.decode.many(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)))),Nat.lte( recover_prefix.b ,191,() List(RLP),RLP.split.length(128,List.concat(U8,List.concat(U8,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value))),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.concat(U8,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
|
||||
//?false-4418-1090-258-258
|
||||
}: List.concat(U8,List.concat(U8, self( () Bytes,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value)))),rlps.head.value),RLP.encode.many(rlps.tail),(bytes) List(RLP),List.nil(RLP),(bytes.head) (bytes.tail) Nat.lte(U8.to_nat(bytes.head),127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,bytes.head,List.nil(U8))),RLP.decode.many(bytes.tail)),Nat.lte(U8.to_nat(bytes.head),191,() List(RLP),RLP.split.length(128,List.concat(U8,List.concat(U8, self( () Bytes,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,rlps.head.value))),List.nil(U8)),List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(128,List.length(U8,Bytes.from_nat(List.length(U8,rlps.head.value)))))),Bytes.from_nat(List.length(U8,rlps.head.value)))),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.concat(U8,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value),RLP.encode.many(rlps.tail)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
|
||||
}! :: RLP.decode.many(List.concat(U8, condition( () List(U8),rlps.head.value,List.concat(U8,RLP.encode.length(128,List.length(U8,rlps.head.value)),rlps.head.value)),RLP.encode.many(rlps.tail))) == List.cons(RLP,RLP.data(rlps.head.value),rlps.tail)
|
||||
node:
|
||||
open bound.snd.fst as bound_child
|
||||
let ind = RLP.encode_identity(rlps.head.child, bound_child.fst)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user