Skip to content

Commit

Permalink
Fix reference to prefix lemma for 'PositiveInteger_ConstSize'
Browse files Browse the repository at this point in the history
  • Loading branch information
mario-bucev committed Sep 8, 2024
1 parent fcebb1d commit af4ddef
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion asn1scala/src/main/scala/asn1scala/asn1jvm_Codec_ACN.scala
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ object ACN {
val (acn2Res, l2) = acn2Reset.dec_Int_PositiveInteger_ConstSize_pure(nBits)

{
BitStream.readNLeastSignificantBitsPrefixLemma(acn1.base.bitStream, acn2.base.bitStream, nBits)
BitStream.readNLSBBitsMSBFirstPrefixLemma(acn1.base.bitStream, acn2.base.bitStream, nBits)
}.ensuring { _ =>
acn1Res.base.bitStream.bitIndex == acn2Res.base.bitStream.bitIndex && l1 == l2
}
Expand Down

0 comments on commit af4ddef

Please sign in to comment.