@@ -632,6 +632,16 @@ builtinsSrc =
632632 mbytearrayt g --> nat --> Type. effect () [g, DD. exceptionType () ] nat,
633633 B " MutableByteArray.read64be" . forall1 " g" $ \ g ->
634634 mbytearrayt g --> nat --> Type. effect () [g, DD. exceptionType () ] nat,
635+ B " MutableByteArray.read16le" . forall1 " g" $ \ g ->
636+ mbytearrayt g --> nat --> Type. effect () [g, DD. exceptionType () ] nat,
637+ B " MutableByteArray.read24le" . forall1 " g" $ \ g ->
638+ mbytearrayt g --> nat --> Type. effect () [g, DD. exceptionType () ] nat,
639+ B " MutableByteArray.read32le" . forall1 " g" $ \ g ->
640+ mbytearrayt g --> nat --> Type. effect () [g, DD. exceptionType () ] nat,
641+ B " MutableByteArray.read40le" . forall1 " g" $ \ g ->
642+ mbytearrayt g --> nat --> Type. effect () [g, DD. exceptionType () ] nat,
643+ B " MutableByteArray.read64le" . forall1 " g" $ \ g ->
644+ mbytearrayt g --> nat --> Type. effect () [g, DD. exceptionType () ] nat,
635645 B " MutableArray.write" . forall2 " g" " a" $ \ g a ->
636646 marrayt g a --> nat --> a --> Type. effect () [g, DD. exceptionType () ] unit,
637647 B " MutableByteArray.write8" . forall1 " g" $ \ g ->
@@ -642,6 +652,12 @@ builtinsSrc =
642652 mbytearrayt g --> nat --> nat --> Type. effect () [g, DD. exceptionType () ] unit,
643653 B " MutableByteArray.write64be" . forall1 " g" $ \ g ->
644654 mbytearrayt g --> nat --> nat --> Type. effect () [g, DD. exceptionType () ] unit,
655+ B " MutableByteArray.write16le" . forall1 " g" $ \ g ->
656+ mbytearrayt g --> nat --> nat --> Type. effect () [g, DD. exceptionType () ] unit,
657+ B " MutableByteArray.write32le" . forall1 " g" $ \ g ->
658+ mbytearrayt g --> nat --> nat --> Type. effect () [g, DD. exceptionType () ] unit,
659+ B " MutableByteArray.write64le" . forall1 " g" $ \ g ->
660+ mbytearrayt g --> nat --> nat --> Type. effect () [g, DD. exceptionType () ] unit,
645661 B " ImmutableArray.copyTo!" . forall2 " g" " a" $ \ g a ->
646662 marrayt g a
647663 --> nat
@@ -670,6 +686,16 @@ builtinsSrc =
670686 ibytearrayt --> nat --> Type. effect1 () (DD. exceptionType () ) nat,
671687 B " ImmutableByteArray.read64be" $
672688 ibytearrayt --> nat --> Type. effect1 () (DD. exceptionType () ) nat,
689+ B " ImmutableByteArray.read16le" $
690+ ibytearrayt --> nat --> Type. effect1 () (DD. exceptionType () ) nat,
691+ B " ImmutableByteArray.read24le" $
692+ ibytearrayt --> nat --> Type. effect1 () (DD. exceptionType () ) nat,
693+ B " ImmutableByteArray.read32le" $
694+ ibytearrayt --> nat --> Type. effect1 () (DD. exceptionType () ) nat,
695+ B " ImmutableByteArray.read40le" $
696+ ibytearrayt --> nat --> Type. effect1 () (DD. exceptionType () ) nat,
697+ B " ImmutableByteArray.read64le" $
698+ ibytearrayt --> nat --> Type. effect1 () (DD. exceptionType () ) nat,
673699 B " MutableArray.freeze!" . forall2 " g" " a" $ \ g a ->
674700 marrayt g a --> Type. effect1 () g (iarrayt a),
675701 B " MutableByteArray.freeze!" . forall1 " g" $ \ g ->
0 commit comments