Remove generated TeX file

1 files changed, 0 insertions, 1810 deletions

diff --git a/lib/isabelle/output/document/Sail2_operators_bitlists.tex b/lib/isabelle/output/document/Sail2_operators_bitlists.tex
deleted file mode 100644
index a676b7bf..00000000
--- a/lib/isabelle/output/document/Sail2_operators_bitlists.tex
+++ /dev/null
@@ -1,1810 +0,0 @@
-%
-\begin{isabellebody}%
-\setisabellecontext{Sail{\isadigit{2}}{\isacharunderscore}operators{\isacharunderscore}bitlists}%
-%
-\isadelimdocument
-%
-\endisadelimdocument
-%
-\isatagdocument
-%
-\isamarkupchapter{Generated by Lem from \isa{{\isachardot}{\isachardot}{\isacharslash}{\isachardot}{\isachardot}{\isacharslash}src{\isacharslash}gen{\isacharunderscore}lib{\isacharslash}sail{\isadigit{2}}{\isacharunderscore}operators{\isacharunderscore}bitlists{\isachardot}lem}.%
-}
-\isamarkuptrue%
-%
-\endisatagdocument
-{\isafolddocument}%
-%
-\isadelimdocument
-%
-\endisadelimdocument
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ {\isachardoublequoteopen}Sail{\isadigit{2}}{\isacharunderscore}operators{\isacharunderscore}bitlists{\isachardoublequoteclose}\ \isanewline
-\isanewline
-\isakeyword{imports}\isanewline
-\ \ Main\isanewline
-\ \ {\isachardoublequoteopen}LEM{\isachardot}Lem{\isacharunderscore}pervasives{\isacharunderscore}extra{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}LEM{\isachardot}Lem{\isacharunderscore}machine{\isacharunderscore}word{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Sail{\isadigit{2}}{\isacharunderscore}values{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Sail{\isadigit{2}}{\isacharunderscore}operators{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Sail{\isadigit{2}}{\isacharunderscore}prompt{\isacharunderscore}monad{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Sail{\isadigit{2}}{\isacharunderscore}prompt{\isachardoublequoteclose}\isanewline
-\isanewline
-\isakeyword{begin}\ \isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{open\ import\ Pervasives{\isacharunderscore}extra}%
-}\isanewline
-%
-\isamarkupcmt{\isa{open\ import\ Machine{\isacharunderscore}word}%
-}\isanewline
-%
-\isamarkupcmt{\isa{open\ import\ Sail{\isadigit{2}}{\isacharunderscore}values}%
-}\isanewline
-%
-\isamarkupcmt{\isa{open\ import\ Sail{\isadigit{2}}{\isacharunderscore}operators}%
-}\isanewline
-%
-\isamarkupcmt{\isa{open\ import\ Sail{\isadigit{2}}{\isacharunderscore}prompt{\isacharunderscore}monad}%
-}\isanewline
-%
-\isamarkupcmt{\isa{open\ import\ Sail{\isadigit{2}}{\isacharunderscore}prompt}%
-}\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{Specialisation\ of\ operators\ to\ bit\ lists}%
-}\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ uint{\isacharunderscore}maybe\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ integer}%
-}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-\isanewline
-%
-\endisadelimtheory
-\isacommand{definition}\isamarkupfalse%
-\ uint{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}int{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ uint{\isacharunderscore}maybe\ v\ {\isacharequal}\ {\isacharparenleft}\ unsigned{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ uint{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}c{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}b{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ uint{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}uint{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}\isanewline
-\ \ {\isacharparenleft}unsigned{\isacharunderscore}method\ \ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a{\isacharparenright}\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ uint{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ uint{\isacharunderscore}nondet\ v\ {\isacharequal}\ {\isacharparenleft}\isanewline
-\ \ bools{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}nondet\ v\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ bs\ {\isachardot}\ \isanewline
-\ \ return\ {\isacharparenleft}int{\isacharunderscore}of{\isacharunderscore}bools\ False\ bs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ uint\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ uint\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}failwith\ {\isacharparenleft}uint{\isacharunderscore}maybe\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ sint{\isacharunderscore}maybe\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ integer}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sint{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}int{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sint{\isacharunderscore}maybe\ v\ {\isacharequal}\ {\isacharparenleft}\ signed{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sint{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}c{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}b{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sint{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}sint{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}\isanewline
-\ \ {\isacharparenleft}signed{\isacharunderscore}method\ \ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a{\isacharparenright}\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sint{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sint{\isacharunderscore}nondet\ v\ {\isacharequal}\ {\isacharparenleft}\isanewline
-\ \ bools{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}nondet\ v\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ bs\ {\isachardot}\ \isanewline
-\ \ return\ {\isacharparenleft}int{\isacharunderscore}of{\isacharunderscore}bools\ True\ bs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sint\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sint\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}failwith\ {\isacharparenleft}sint{\isacharunderscore}maybe\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ extz{\isacharunderscore}vec\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ extz{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ extz{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ extz{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ exts{\isacharunderscore}vec\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ exts{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ exts{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ exts{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ zero{\isacharunderscore}extend\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ zero{\isacharunderscore}extend\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ zero{\isacharunderscore}extend\ bits\ len\ {\isacharequal}\ {\isacharparenleft}\ extz{\isacharunderscore}bits\ len\ bits\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ sign{\isacharunderscore}extend\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sign{\isacharunderscore}extend\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sign{\isacharunderscore}extend\ bits\ len\ {\isacharequal}\ {\isacharparenleft}\ exts{\isacharunderscore}bits\ len\ bits\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ zeros\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ zeros\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ zeros\ len\ {\isacharequal}\ {\isacharparenleft}\ repeat\ {\isacharbrackleft}B{\isadigit{0}}{\isacharbrackright}\ len\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ vector{\isacharunderscore}truncate\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ vector{\isacharunderscore}truncate\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ vector{\isacharunderscore}truncate\ bs\ len\ {\isacharequal}\ {\isacharparenleft}\ extz{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ len\ bs\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}maybe\ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}fail\ \ \ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}nondet\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}failwith\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bits\ \ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ access{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ access{\isacharunderscore}vec{\isacharunderscore}inc\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ access{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ access{\isacharunderscore}bv{\isacharunderscore}inc\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ access{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ access{\isacharunderscore}vec{\isacharunderscore}dec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ access{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ access{\isacharunderscore}bv{\isacharunderscore}dec\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ update{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ update{\isacharunderscore}vec{\isacharunderscore}inc\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ update{\isacharunderscore}bv{\isacharunderscore}inc\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}maybe\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}inc\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}fail\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}inc\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}nondet\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}inc\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ update{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ update{\isacharunderscore}vec{\isacharunderscore}dec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ update{\isacharunderscore}bv{\isacharunderscore}dec\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}maybe\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}dec\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}fail\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}dec\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}nondet\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}dec\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ subrange{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ subrange{\isacharunderscore}vec{\isacharunderscore}inc\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ subrange{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ subrange{\isacharunderscore}bv{\isacharunderscore}inc\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ subrange{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ subrange{\isacharunderscore}vec{\isacharunderscore}dec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ subrange{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ subrange{\isacharunderscore}bv{\isacharunderscore}dec\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}inc\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ update{\isacharunderscore}subrange{\isacharunderscore}bv{\isacharunderscore}inc\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}dec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ update{\isacharunderscore}subrange{\isacharunderscore}bv{\isacharunderscore}dec\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ concat{\isacharunderscore}vec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ concat{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ concat{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ concat{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ cons{\isacharunderscore}vec\ {\isacharcolon}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ cons{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ cons{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ cons{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ cons{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ cons{\isacharunderscore}vec{\isacharunderscore}maybe\ b\ v\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}cons{\isacharunderscore}vec\ b\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ cons{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ cons{\isacharunderscore}vec{\isacharunderscore}fail\ b\ v\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}cons{\isacharunderscore}vec\ b\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ cons{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ cons{\isacharunderscore}vec{\isacharunderscore}nondet\ b\ v\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}cons{\isacharunderscore}vec\ b\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ cast{\isacharunderscore}unit{\isacharunderscore}vec\ {\isacharcolon}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ cast{\isacharunderscore}unit{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ cast{\isacharunderscore}unit{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ cast{\isacharunderscore}unit{\isacharunderscore}bv\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}maybe\ b\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}cast{\isacharunderscore}unit{\isacharunderscore}vec\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}fail\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}cast{\isacharunderscore}unit{\isacharunderscore}vec\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}nondet\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}cast{\isacharunderscore}unit{\isacharunderscore}vec\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bit\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ vec{\isacharunderscore}of{\isacharunderscore}bit\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ vec{\isacharunderscore}of{\isacharunderscore}bit\ {\isacharequal}\ {\isacharparenleft}\ bv{\isacharunderscore}of{\isacharunderscore}bit\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}maybe\ len\ b\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}vec{\isacharunderscore}of{\isacharunderscore}bit\ len\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}fail\ len\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}vec{\isacharunderscore}of{\isacharunderscore}bit\ len\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}nondet\ len\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}vec{\isacharunderscore}of{\isacharunderscore}bit\ len\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ msb\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ msb\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bitU\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ msb\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ most{\isacharunderscore}significant\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}maybe\ {\isacharcolon}\ bool\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ integer}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bool\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}int{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}maybe\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ int{\isacharunderscore}of{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bool\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}fail\ sign\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}int{\isacharunderscore}of{\isacharunderscore}vec{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}maybe\ sign\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bool\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}nondet\ sign\ v\ {\isacharequal}\ {\isacharparenleft}\ bools{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}nondet\ v\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ v\ {\isachardot}\ \ return\ {\isacharparenleft}int{\isacharunderscore}of{\isacharunderscore}bools\ sign\ v{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ int{\isacharunderscore}of{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bool\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ int{\isacharunderscore}of{\isacharunderscore}vec\ sign\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}failwith\ {\isacharparenleft}int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}maybe\ sign\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ string{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ string}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ string{\isacharunderscore}of{\isacharunderscore}bits\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ string\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ string{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ string{\isacharunderscore}of{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ decimal{\isacharunderscore}string{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ string}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ decimal{\isacharunderscore}string{\isacharunderscore}of{\isacharunderscore}bits\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ string\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ decimal{\isacharunderscore}string{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ decimal{\isacharunderscore}string{\isacharunderscore}of{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ and{\isacharunderscore}vec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ or{\isacharunderscore}vec\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ xor{\isacharunderscore}vec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ not{\isacharunderscore}vec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ and{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ and{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ binop{\isacharunderscore}list\ and{\isacharunderscore}bit\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ or{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ or{\isacharunderscore}vec\ \ {\isacharequal}\ {\isacharparenleft}\ binop{\isacharunderscore}list\ or{\isacharunderscore}bit\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ xor{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ xor{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ binop{\isacharunderscore}list\ xor{\isacharunderscore}bit\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ not{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ not{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ List{\isachardot}map\ not{\isacharunderscore}bit\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ {\isacharcolon}\ forall\ {\isacharprime}a\ {\isacharprime}b{\isachardot}\ Bitvector\ {\isacharprime}a\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer{\isacharparenright}\ {\isacharminus}{\isachargreater}\ bool\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}{\isacharparenleft}int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isacharparenright}{\isasymRightarrow}\ bool\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ op{\isadigit{1}}\ sign\ l\ r\ {\isacharequal}\ {\isacharparenleft}\isanewline
-\ \ {\isacharparenleft}let\ len\ {\isacharequal}{\isacharparenleft}{\isacharparenleft}\ {\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}\ {\isacharasterisk}\isanewline
-\ \ {\isacharparenleft}length{\isacharunderscore}method\ \ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a{\isacharparenright}\ l{\isacharparenright}\ in\isanewline
-\ \ {\isacharparenleft}let\ l{\isacharprime}\ {\isacharequal}\ {\isacharparenleft}if\ sign\ then\ exts{\isacharunderscore}bv\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ len\ l\ else\ extz{\isacharunderscore}bv\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ len\ l{\isacharparenright}\ in\isanewline
-\ \ {\isacharparenleft}let\ r{\isacharprime}\ {\isacharequal}\ {\isacharparenleft}if\ sign\ then\ exts{\isacharunderscore}bv\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ len\ r\ else\ extz{\isacharunderscore}bv\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ len\ r{\isacharparenright}\ in\isanewline
-\ \ List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}arith{\isacharunderscore}op{\isacharunderscore}bits\ op{\isadigit{1}}\ sign\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ l{\isacharprime}{\isacharparenright}\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ r{\isacharprime}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ add{\isacharunderscore}vec\ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ adds{\isacharunderscore}vec\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ sub{\isacharunderscore}vec\ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ subs{\isacharunderscore}vec\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ mult{\isacharunderscore}vec\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ mults{\isacharunderscore}vec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ add{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec\ \ \ {\isacharequal}\ {\isacharparenleft}\ {\isacharparenleft}{\isasymlambda}\ l\ r{\isachardot}\ List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}arith{\isacharunderscore}op{\isacharunderscore}bits\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ False\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ l{\isacharparenright}\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ adds{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec\ \ {\isacharequal}\ {\isacharparenleft}\ {\isacharparenleft}{\isasymlambda}\ l\ r{\isachardot}\ List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}arith{\isacharunderscore}op{\isacharunderscore}bits\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ True\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ l{\isacharparenright}\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sub{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec\ \ \ {\isacharequal}\ {\isacharparenleft}\ {\isacharparenleft}{\isasymlambda}\ l\ r{\isachardot}\ List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}arith{\isacharunderscore}op{\isacharunderscore}bits\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ False\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ l{\isacharparenright}\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ subs{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec\ \ {\isacharequal}\ {\isacharparenleft}\ {\isacharparenleft}{\isasymlambda}\ l\ r{\isachardot}\ List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}arith{\isacharunderscore}op{\isacharunderscore}bits\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ True\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ l{\isacharparenright}\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mult{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mult{\isacharunderscore}vec\ \ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}\ {\isacharasterisk}\ {\isacharparenright}\ False\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mults{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mults{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}\ {\isacharasterisk}\ {\isacharparenright}\ True\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ add{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ sub{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ mult{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ add{\isacharunderscore}vec{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}int\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sub{\isacharunderscore}vec{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}int\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mult{\isacharunderscore}vec{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mult{\isacharunderscore}vec{\isacharunderscore}int\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}\ {\isacharasterisk}\ {\isacharparenright}\ False\ l\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}bits{\isacharunderscore}of{\isacharunderscore}int\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ add{\isacharunderscore}int{\isacharunderscore}vec\ \ \ \ \ \ \ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ sub{\isacharunderscore}int{\isacharunderscore}vec\ \ \ \ \ \ \ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ mult{\isacharunderscore}int{\isacharunderscore}vec\ \ \ \ \ \ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ add{\isacharunderscore}int{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}int{\isacharunderscore}vec\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}int{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sub{\isacharunderscore}int{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}int{\isacharunderscore}vec\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}int{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mult{\isacharunderscore}int{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mult{\isacharunderscore}int{\isacharunderscore}vec\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}\ {\isacharasterisk}\ {\isacharparenright}\ False\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}bits{\isacharunderscore}of{\isacharunderscore}int\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ r{\isacharparenright}{\isacharparenright}\ l{\isacharparenright}{\isacharparenright}\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ add{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ adds{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ sub{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ subs{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ add{\isacharunderscore}vec{\isacharunderscore}bool\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ {\isacharprime}a\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}bool\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bool\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bit\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ bool{\isacharunderscore}of{\isacharunderscore}bitU{\isacharunderscore}nondet\ r\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ r\ {\isachardot}\ \ return\ {\isacharparenleft}add{\isacharunderscore}vec{\isacharunderscore}bool\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ add{\isacharunderscore}vec{\isacharunderscore}bit\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ adds{\isacharunderscore}vec{\isacharunderscore}bool\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ {\isacharprime}a\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec{\isacharunderscore}bool\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bool\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ True\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bit\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ True\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ bool{\isacharunderscore}of{\isacharunderscore}bitU{\isacharunderscore}nondet\ r\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ r\ {\isachardot}\ \ return\ {\isacharparenleft}adds{\isacharunderscore}vec{\isacharunderscore}bool\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ adds{\isacharunderscore}vec{\isacharunderscore}bit\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sub{\isacharunderscore}vec{\isacharunderscore}bool\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ {\isacharprime}a\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}bool\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bool\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bit\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ bool{\isacharunderscore}of{\isacharunderscore}bitU{\isacharunderscore}nondet\ r\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ r\ {\isachardot}\ \ return\ {\isacharparenleft}sub{\isacharunderscore}vec{\isacharunderscore}bool\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ sub{\isacharunderscore}vec{\isacharunderscore}bit\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ subs{\isacharunderscore}vec{\isacharunderscore}bool\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ {\isacharprime}a\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec{\isacharunderscore}bool\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bool\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ True\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bit\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ True\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ bool{\isacharunderscore}of{\isacharunderscore}bitU{\isacharunderscore}nondet\ r\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ r\ {\isachardot}\ \ return\ {\isacharparenleft}subs{\isacharunderscore}vec{\isacharunderscore}bool\ \isanewline
-\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ subs{\isacharunderscore}vec{\isacharunderscore}bit\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ add{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ sub{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ mult{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ mult{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ let\ add{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ \ {\isacharequal}\ add{\isacharunderscore}overflow{\isacharunderscore}bv\ let\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ \ {\isacharequal}\ add{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}signed\ let\ sub{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ \ {\isacharequal}\ sub{\isacharunderscore}overflow{\isacharunderscore}bv\ let\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ \ {\isacharequal}\ sub{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}signed\ let\ mult{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ {\isacharequal}\ mult{\isacharunderscore}overflow{\isacharunderscore}bv\ let\ mult{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ {\isacharequal}\ mult{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}signed\ \ val\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}signed\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}signed\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ let\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ \ {\isacharequal}\ add{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}bit\ let\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}signed\ \ {\isacharequal}\ add{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}bit{\isacharunderscore}signed\ let\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ \ {\isacharequal}\ sub{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}bit\ let\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}signed\ \ {\isacharequal}\ sub{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}bit{\isacharunderscore}signed}%
-}\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ shiftl\ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ shiftr\ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ arith{\isacharunderscore}shiftr\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ rotl\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ rotr\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ shiftl\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \ \ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ shiftl\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ shiftl{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ shiftr\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \ \ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ shiftr\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ shiftr{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ arith{\isacharunderscore}shiftr\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ arith{\isacharunderscore}shiftr\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ arith{\isacharunderscore}shiftr{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ rotl\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \ \ \ \ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ rotl\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ rotl{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ rotr\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \ \ \ \ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ rotr\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ rotr{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}nondet\ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mod{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}mod{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mod{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}maybe\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ mod{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mod{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}mod{\isacharunderscore}vec{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}mod{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mod{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}nondet\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ of{\isacharunderscore}bits{\isacharunderscore}nondet\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}mod{\isacharunderscore}vec\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}nondet\ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quot{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}quot{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quot{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}maybe\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ quot{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quot{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}quot{\isacharunderscore}vec{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}quot{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quot{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}nondet\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ of{\isacharunderscore}bits{\isacharunderscore}nondet\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}quot{\isacharunderscore}vec\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ quots{\isacharunderscore}vec\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ quots{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ quots{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ quots{\isacharunderscore}vec{\isacharunderscore}nondet\ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quots{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quots{\isacharunderscore}vec\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}quots{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quots{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quots{\isacharunderscore}vec{\isacharunderscore}maybe\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ quots{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quots{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quots{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}quots{\isacharunderscore}vec{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}quots{\isacharunderscore}bv\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quots{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quots{\isacharunderscore}vec{\isacharunderscore}nondet\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ of{\isacharunderscore}bits{\isacharunderscore}nondet\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}quots{\isacharunderscore}vec\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mod{\isacharunderscore}vec{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}mod{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ mod{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}mod{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ of{\isacharunderscore}bits{\isacharunderscore}nondet\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}mod{\isacharunderscore}vec{\isacharunderscore}int\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quot{\isacharunderscore}vec{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}quot{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ quot{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}quot{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ of{\isacharunderscore}bits{\isacharunderscore}nondet\ \isanewline
-\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}quot{\isacharunderscore}vec{\isacharunderscore}int\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ replicate{\isacharunderscore}bits\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ replicate{\isacharunderscore}bits\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ replicate{\isacharunderscore}bits\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ replicate{\isacharunderscore}bits{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ duplicate\ {\isacharcolon}\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ duplicate\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ duplicate\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ duplicate{\isacharunderscore}bit{\isacharunderscore}bv\ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ duplicate{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ duplicate{\isacharunderscore}maybe\ b\ n\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}duplicate\ b\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ duplicate{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ duplicate{\isacharunderscore}fail\ b\ n\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}duplicate\ b\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ duplicate{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ duplicate{\isacharunderscore}nondet\ b\ n\ {\isacharequal}\ {\isacharparenleft}\isanewline
-\ \ bool{\isacharunderscore}of{\isacharunderscore}bitU{\isacharunderscore}nondet\ b\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ b\ {\isachardot}\ \isanewline
-\ \ return\ {\isacharparenleft}duplicate\ {\isacharparenleft}bitU{\isacharunderscore}of{\isacharunderscore}bool\ b{\isacharparenright}\ n{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ reverse{\isacharunderscore}endianness\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ reverse{\isacharunderscore}endianness\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ reverse{\isacharunderscore}endianness\ v\ {\isacharequal}\ {\isacharparenleft}\ reverse{\isacharunderscore}endianness{\isacharunderscore}list\ v\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ get{\isacharunderscore}slice{\isacharunderscore}int\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ get{\isacharunderscore}slice{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ get{\isacharunderscore}slice{\isacharunderscore}int\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ get{\isacharunderscore}slice{\isacharunderscore}int{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ set{\isacharunderscore}slice{\isacharunderscore}int\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ set{\isacharunderscore}slice{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ set{\isacharunderscore}slice{\isacharunderscore}int\ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ set{\isacharunderscore}slice{\isacharunderscore}int{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ slice\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ slice\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ slice\ v\ lo\ len\ {\isacharequal}\ {\isacharparenleft}\isanewline
-\ \ subrange{\isacharunderscore}vec{\isacharunderscore}dec\ v\ {\isacharparenleft}{\isacharparenleft}lo\ {\isacharplus}\ len{\isacharparenright}\ {\isacharminus}{\isacharparenleft}\ {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isacharparenright}\ lo\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ set{\isacharunderscore}slice\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ set{\isacharunderscore}slice\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ set{\isacharunderscore}slice\ {\isacharparenleft}out{\isacharunderscore}len{\isacharcolon}{\isacharcolon}ii{\isacharparenright}\ {\isacharparenleft}slice{\isacharunderscore}len{\isacharcolon}{\isacharcolon}ii{\isacharparenright}\ out\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}ii{\isacharparenright}\ v\ {\isacharequal}\ {\isacharparenleft}\isanewline
-\ \ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}dec\ out\ {\isacharparenleft}{\isacharparenleft}n\ {\isacharplus}\ slice{\isacharunderscore}len{\isacharparenright}\ {\isacharminus}{\isacharparenleft}\ {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isacharparenright}\ n\ v\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isanewline
-%
-\isamarkupcmt{\isa{val\ eq{\isacharunderscore}vec\ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bool}%
-}\isanewline
-%
-\isamarkupcmt{\isa{val\ neq{\isacharunderscore}vec\ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bool}%
-}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ eq{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bool\ {\isachardoublequoteclose}\ \ \ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ eq{\isacharunderscore}vec\ \ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ eq{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ neq{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bool\ {\isachardoublequoteclose}\ \ \ \ \isakeyword{where}\ \isanewline
-\ \ \ \ \ {\isachardoublequoteopen}\ neq{\isacharunderscore}vec\ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline
-\ \ neq{\isacharunderscore}bv\isanewline
-\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline
-\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimtheory
-\isanewline
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\end{isabellebody}%
-\endinput
-%:%file=~/workspace/uni/rems/github/sail/lib/isabelle/Sail2_operators_bitlists.thy%:%
-%:%11=1%:%
-%:%27=3%:%
-%:%28=3%:%
-%:%29=4%:%
-%:%30=5%:%
-%:%31=6%:%
-%:%32=7%:%
-%:%33=8%:%
-%:%34=9%:%
-%:%35=10%:%
-%:%36=11%:%
-%:%37=12%:%
-%:%38=13%:%
-%:%39=14%:%
-%:%40=15%:%
-%:%43=16%:%
-%:%46=17%:%
-%:%49=18%:%
-%:%52=19%:%
-%:%55=20%:%
-%:%58=21%:%
-%:%59=22%:%
-%:%62=23%:%
-%:%63=24%:%
-%:%71=25%:%
-%:%74=26%:%
-%:%75=26%:%
-%:%76=27%:%
-%:%77=28%:%
-%:%78=29%:%
-%:%79=29%:%
-%:%80=30%:%
-%:%81=31%:%
-%:%82=32%:%
-%:%83=33%:%
-%:%84=33%:%
-%:%85=34%:%
-%:%87=36%:%
-%:%88=37%:%
-%:%89=38%:%
-%:%90=38%:%
-%:%91=39%:%
-%:%92=40%:%
-%:%93=41%:%
-%:%96=42%:%
-%:%97=43%:%
-%:%98=43%:%
-%:%99=44%:%
-%:%100=45%:%
-%:%101=46%:%
-%:%102=46%:%
-%:%103=47%:%
-%:%104=48%:%
-%:%105=49%:%
-%:%106=50%:%
-%:%107=50%:%
-%:%108=51%:%
-%:%110=53%:%
-%:%111=54%:%
-%:%112=55%:%
-%:%113=55%:%
-%:%114=56%:%
-%:%115=57%:%
-%:%116=58%:%
-%:%119=59%:%
-%:%120=60%:%
-%:%121=60%:%
-%:%122=61%:%
-%:%125=64%:%
-%:%126=65%:%
-%:%127=66%:%
-%:%130=67%:%
-%:%131=68%:%
-%:%132=68%:%
-%:%133=69%:%
-%:%136=72%:%
-%:%137=73%:%
-%:%138=74%:%
-%:%141=75%:%
-%:%142=76%:%
-%:%143=76%:%
-%:%144=77%:%
-%:%145=78%:%
-%:%146=79%:%
-%:%149=80%:%
-%:%150=81%:%
-%:%151=81%:%
-%:%152=82%:%
-%:%153=83%:%
-%:%154=84%:%
-%:%157=85%:%
-%:%158=86%:%
-%:%159=86%:%
-%:%160=87%:%
-%:%161=88%:%
-%:%162=89%:%
-%:%165=90%:%
-%:%166=91%:%
-%:%167=91%:%
-%:%168=92%:%
-%:%170=94%:%
-%:%171=95%:%
-%:%172=96%:%
-%:%175=97%:%
-%:%178=98%:%
-%:%181=99%:%
-%:%184=100%:%
-%:%187=101%:%
-%:%188=102%:%
-%:%191=103%:%
-%:%192=104%:%
-%:%193=104%:%
-%:%194=105%:%
-%:%197=108%:%
-%:%198=109%:%
-%:%199=110%:%
-%:%202=111%:%
-%:%203=112%:%
-%:%204=112%:%
-%:%205=113%:%
-%:%208=116%:%
-%:%209=117%:%
-%:%210=118%:%
-%:%213=119%:%
-%:%214=120%:%
-%:%215=120%:%
-%:%216=121%:%
-%:%219=124%:%
-%:%220=125%:%
-%:%221=126%:%
-%:%222=126%:%
-%:%223=127%:%
-%:%224=128%:%
-%:%225=129%:%
-%:%226=129%:%
-%:%227=130%:%
-%:%228=131%:%
-%:%229=132%:%
-%:%230=132%:%
-%:%231=133%:%
-%:%232=134%:%
-%:%233=135%:%
-%:%236=136%:%
-%:%237=137%:%
-%:%238=137%:%
-%:%239=138%:%
-%:%242=141%:%
-%:%243=142%:%
-%:%244=143%:%
-%:%245=143%:%
-%:%246=144%:%
-%:%247=145%:%
-%:%248=146%:%
-%:%249=146%:%
-%:%250=147%:%
-%:%251=148%:%
-%:%252=149%:%
-%:%253=149%:%
-%:%254=150%:%
-%:%255=151%:%
-%:%256=152%:%
-%:%259=153%:%
-%:%260=154%:%
-%:%261=154%:%
-%:%262=155%:%
-%:%265=158%:%
-%:%266=159%:%
-%:%267=160%:%
-%:%270=161%:%
-%:%271=162%:%
-%:%272=162%:%
-%:%273=163%:%
-%:%276=166%:%
-%:%277=167%:%
-%:%278=168%:%
-%:%281=169%:%
-%:%282=170%:%
-%:%283=170%:%
-%:%284=171%:%
-%:%289=176%:%
-%:%290=177%:%
-%:%291=178%:%
-%:%294=179%:%
-%:%295=180%:%
-%:%296=180%:%
-%:%297=181%:%
-%:%302=186%:%
-%:%303=187%:%
-%:%304=188%:%
-%:%307=189%:%
-%:%308=190%:%
-%:%309=190%:%
-%:%310=191%:%
-%:%315=196%:%
-%:%316=197%:%
-%:%317=198%:%
-%:%320=199%:%
-%:%321=200%:%
-%:%322=200%:%
-%:%323=201%:%
-%:%326=204%:%
-%:%327=205%:%
-%:%328=206%:%
-%:%329=206%:%
-%:%330=207%:%
-%:%331=208%:%
-%:%332=209%:%
-%:%333=209%:%
-%:%334=210%:%
-%:%335=211%:%
-%:%336=212%:%
-%:%337=212%:%
-%:%338=213%:%
-%:%339=214%:%
-%:%340=215%:%
-%:%343=216%:%
-%:%344=217%:%
-%:%345=217%:%
-%:%346=218%:%
-%:%347=219%:%
-%:%348=220%:%
-%:%349=220%:%
-%:%350=221%:%
-%:%351=222%:%
-%:%352=223%:%
-%:%353=223%:%
-%:%354=224%:%
-%:%355=225%:%
-%:%356=226%:%
-%:%357=226%:%
-%:%358=227%:%
-%:%359=228%:%
-%:%360=229%:%
-%:%363=230%:%
-%:%364=231%:%
-%:%365=231%:%
-%:%366=232%:%
-%:%367=233%:%
-%:%368=234%:%
-%:%369=234%:%
-%:%370=235%:%
-%:%371=236%:%
-%:%372=237%:%
-%:%373=237%:%
-%:%374=238%:%
-%:%375=239%:%
-%:%376=240%:%
-%:%377=240%:%
-%:%378=241%:%
-%:%379=242%:%
-%:%380=243%:%
-%:%383=244%:%
-%:%384=245%:%
-%:%385=245%:%
-%:%386=246%:%
-%:%389=249%:%
-%:%390=250%:%
-%:%391=251%:%
-%:%394=252%:%
-%:%395=253%:%
-%:%396=253%:%
-%:%397=254%:%
-%:%400=257%:%
-%:%401=258%:%
-%:%402=259%:%
-%:%403=259%:%
-%:%404=260%:%
-%:%405=261%:%
-%:%406=262%:%
-%:%407=262%:%
-%:%408=263%:%
-%:%409=264%:%
-%:%410=265%:%
-%:%411=265%:%
-%:%412=266%:%
-%:%413=267%:%
-%:%414=268%:%
-%:%417=269%:%
-%:%418=270%:%
-%:%419=270%:%
-%:%420=271%:%
-%:%423=274%:%
-%:%424=275%:%
-%:%425=276%:%
-%:%428=277%:%
-%:%429=278%:%
-%:%430=278%:%
-%:%431=279%:%
-%:%434=282%:%
-%:%435=283%:%
-%:%436=284%:%
-%:%439=285%:%
-%:%442=286%:%
-%:%445=287%:%
-%:%448=288%:%
-%:%449=289%:%
-%:%450=289%:%
-%:%451=290%:%
-%:%452=291%:%
-%:%453=292%:%
-%:%454=292%:%
-%:%455=293%:%
-%:%456=294%:%
-%:%457=295%:%
-%:%458=295%:%
-%:%459=296%:%
-%:%460=297%:%
-%:%461=298%:%
-%:%462=298%:%
-%:%463=299%:%
-%:%464=300%:%
-%:%465=301%:%
-%:%468=303%:%
-%:%469=304%:%
-%:%470=304%:%
-%:%471=305%:%
-%:%478=312%:%
-%:%479=313%:%
-%:%480=314%:%
-%:%483=315%:%
-%:%486=316%:%
-%:%489=317%:%
-%:%492=318%:%
-%:%495=319%:%
-%:%498=320%:%
-%:%499=321%:%
-%:%500=321%:%
-%:%501=322%:%
-%:%502=323%:%
-%:%503=324%:%
-%:%504=324%:%
-%:%505=325%:%
-%:%506=326%:%
-%:%507=327%:%
-%:%508=327%:%
-%:%509=328%:%
-%:%510=329%:%
-%:%511=330%:%
-%:%512=330%:%
-%:%513=331%:%
-%:%514=332%:%
-%:%515=333%:%
-%:%516=333%:%
-%:%517=334%:%
-%:%519=336%:%
-%:%520=337%:%
-%:%521=338%:%
-%:%522=338%:%
-%:%523=339%:%
-%:%525=341%:%
-%:%526=342%:%
-%:%527=343%:%
-%:%530=344%:%
-%:%533=345%:%
-%:%536=346%:%
-%:%537=347%:%
-%:%538=347%:%
-%:%539=348%:%
-%:%541=350%:%
-%:%542=351%:%
-%:%543=352%:%
-%:%544=352%:%
-%:%545=353%:%
-%:%547=355%:%
-%:%548=356%:%
-%:%549=357%:%
-%:%550=357%:%
-%:%551=358%:%
-%:%553=360%:%
-%:%554=361%:%
-%:%555=362%:%
-%:%558=363%:%
-%:%561=364%:%
-%:%564=365%:%
-%:%565=366%:%
-%:%566=366%:%
-%:%567=367%:%
-%:%569=369%:%
-%:%570=370%:%
-%:%571=371%:%
-%:%572=371%:%
-%:%573=372%:%
-%:%575=374%:%
-%:%576=375%:%
-%:%577=376%:%
-%:%578=376%:%
-%:%579=377%:%
-%:%581=379%:%
-%:%582=380%:%
-%:%583=381%:%
-%:%586=382%:%
-%:%589=383%:%
-%:%592=384%:%
-%:%595=385%:%
-%:%596=386%:%
-%:%597=387%:%
-%:%598=387%:%
-%:%599=388%:%
-%:%600=389%:%
-%:%601=390%:%
-%:%602=391%:%
-%:%603=391%:%
-%:%604=392%:%
-%:%605=393%:%
-%:%606=394%:%
-%:%607=395%:%
-%:%608=395%:%
-%:%609=396%:%
-%:%610=397%:%
-%:%611=398%:%
-%:%612=399%:%
-%:%613=399%:%
-%:%614=400%:%
-%:%615=401%:%
-%:%616=402%:%
-%:%617=403%:%
-%:%618=403%:%
-%:%619=404%:%
-%:%621=406%:%
-%:%622=407%:%
-%:%623=408%:%
-%:%624=409%:%
-%:%625=409%:%
-%:%626=410%:%
-%:%627=411%:%
-%:%628=412%:%
-%:%629=413%:%
-%:%630=413%:%
-%:%631=414%:%
-%:%632=415%:%
-%:%633=416%:%
-%:%634=417%:%
-%:%635=417%:%
-%:%636=418%:%
-%:%637=419%:%
-%:%638=420%:%
-%:%639=421%:%
-%:%640=421%:%
-%:%641=422%:%
-%:%642=423%:%
-%:%643=424%:%
-%:%644=425%:%
-%:%645=425%:%
-%:%646=426%:%
-%:%648=428%:%
-%:%649=429%:%
-%:%650=430%:%
-%:%651=431%:%
-%:%652=431%:%
-%:%653=432%:%
-%:%654=433%:%
-%:%655=434%:%
-%:%656=435%:%
-%:%657=435%:%
-%:%658=436%:%
-%:%659=437%:%
-%:%660=438%:%
-%:%661=439%:%
-%:%662=439%:%
-%:%663=440%:%
-%:%664=441%:%
-%:%665=442%:%
-%:%666=443%:%
-%:%667=443%:%
-%:%668=444%:%
-%:%669=445%:%
-%:%670=446%:%
-%:%671=447%:%
-%:%672=447%:%
-%:%673=448%:%
-%:%675=450%:%
-%:%676=451%:%
-%:%677=452%:%
-%:%678=453%:%
-%:%679=453%:%
-%:%680=454%:%
-%:%681=455%:%
-%:%682=456%:%
-%:%683=457%:%
-%:%684=457%:%
-%:%685=458%:%
-%:%686=459%:%
-%:%687=460%:%
-%:%688=461%:%
-%:%689=461%:%
-%:%690=462%:%
-%:%691=463%:%
-%:%692=464%:%
-%:%693=465%:%
-%:%694=465%:%
-%:%695=466%:%
-%:%696=467%:%
-%:%697=468%:%
-%:%698=469%:%
-%:%699=469%:%
-%:%700=470%:%
-%:%702=472%:%
-%:%703=473%:%
-%:%704=474%:%
-%:%707=495%:%
-%:%708=496%:%
-%:%711=497%:%
-%:%714=498%:%
-%:%717=499%:%
-%:%720=500%:%
-%:%723=501%:%
-%:%724=502%:%
-%:%725=502%:%
-%:%726=503%:%
-%:%729=506%:%
-%:%730=507%:%
-%:%731=508%:%
-%:%732=508%:%
-%:%733=509%:%
-%:%736=512%:%
-%:%737=513%:%
-%:%738=514%:%
-%:%739=514%:%
-%:%740=515%:%
-%:%743=518%:%
-%:%744=519%:%
-%:%745=520%:%
-%:%746=520%:%
-%:%747=521%:%
-%:%750=524%:%
-%:%751=525%:%
-%:%752=526%:%
-%:%753=526%:%
-%:%754=527%:%
-%:%757=530%:%
-%:%758=531%:%
-%:%759=532%:%
-%:%762=533%:%
-%:%765=534%:%
-%:%768=535%:%
-%:%771=536%:%
-%:%772=537%:%
-%:%773=537%:%
-%:%774=538%:%
-%:%777=541%:%
-%:%778=542%:%
-%:%779=543%:%
-%:%780=543%:%
-%:%781=544%:%
-%:%784=547%:%
-%:%785=548%:%
-%:%786=549%:%
-%:%787=549%:%
-%:%788=550%:%
-%:%791=553%:%
-%:%792=554%:%
-%:%793=555%:%
-%:%794=555%:%
-%:%795=556%:%
-%:%797=558%:%
-%:%798=559%:%
-%:%799=560%:%
-%:%802=561%:%
-%:%805=562%:%
-%:%808=563%:%
-%:%811=564%:%
-%:%812=565%:%
-%:%813=565%:%
-%:%814=566%:%
-%:%817=569%:%
-%:%818=570%:%
-%:%819=571%:%
-%:%820=571%:%
-%:%821=572%:%
-%:%824=575%:%
-%:%825=576%:%
-%:%826=577%:%
-%:%827=577%:%
-%:%828=578%:%
-%:%831=581%:%
-%:%832=582%:%
-%:%833=583%:%
-%:%834=583%:%
-%:%835=584%:%
-%:%837=586%:%
-%:%838=587%:%
-%:%839=588%:%
-%:%842=589%:%
-%:%845=590%:%
-%:%848=591%:%
-%:%851=592%:%
-%:%852=593%:%
-%:%853=593%:%
-%:%854=594%:%
-%:%857=597%:%
-%:%858=598%:%
-%:%859=599%:%
-%:%860=599%:%
-%:%861=600%:%
-%:%864=603%:%
-%:%865=604%:%
-%:%866=605%:%
-%:%867=605%:%
-%:%868=606%:%
-%:%871=609%:%
-%:%872=610%:%
-%:%873=611%:%
-%:%874=611%:%
-%:%875=612%:%
-%:%877=614%:%
-%:%878=615%:%
-%:%879=616%:%
-%:%882=617%:%
-%:%885=618%:%
-%:%888=619%:%
-%:%891=620%:%
-%:%892=621%:%
-%:%893=621%:%
-%:%894=622%:%
-%:%897=625%:%
-%:%898=626%:%
-%:%899=627%:%
-%:%900=627%:%
-%:%901=628%:%
-%:%904=631%:%
-%:%905=632%:%
-%:%906=633%:%
-%:%907=633%:%
-%:%908=634%:%
-%:%911=637%:%
-%:%912=638%:%
-%:%913=639%:%
-%:%914=639%:%
-%:%915=640%:%
-%:%917=642%:%
-%:%918=643%:%
-%:%919=644%:%
-%:%922=645%:%
-%:%925=646%:%
-%:%928=647%:%
-%:%931=648%:%
-%:%932=649%:%
-%:%933=649%:%
-%:%934=650%:%
-%:%937=653%:%
-%:%938=654%:%
-%:%939=655%:%
-%:%940=655%:%
-%:%941=656%:%
-%:%944=659%:%
-%:%945=660%:%
-%:%946=661%:%
-%:%947=661%:%
-%:%948=662%:%
-%:%951=665%:%
-%:%952=666%:%
-%:%953=667%:%
-%:%954=667%:%
-%:%955=668%:%
-%:%957=670%:%
-%:%958=671%:%
-%:%959=672%:%
-%:%962=673%:%
-%:%963=674%:%
-%:%964=674%:%
-%:%965=675%:%
-%:%968=678%:%
-%:%969=679%:%
-%:%970=680%:%
-%:%973=681%:%
-%:%974=682%:%
-%:%975=682%:%
-%:%976=683%:%
-%:%977=684%:%
-%:%978=685%:%
-%:%979=686%:%
-%:%980=686%:%
-%:%981=687%:%
-%:%982=688%:%
-%:%983=689%:%
-%:%984=689%:%
-%:%985=690%:%
-%:%986=691%:%
-%:%987=692%:%
-%:%988=692%:%
-%:%989=693%:%
-%:%991=695%:%
-%:%992=696%:%
-%:%993=697%:%
-%:%996=698%:%
-%:%997=699%:%
-%:%998=699%:%
-%:%999=700%:%
-%:%1000=701%:%
-%:%1001=702%:%
-%:%1004=703%:%
-%:%1005=704%:%
-%:%1006=704%:%
-%:%1007=705%:%
-%:%1010=708%:%
-%:%1011=709%:%
-%:%1012=710%:%
-%:%1015=711%:%
-%:%1016=712%:%
-%:%1017=712%:%
-%:%1018=713%:%
-%:%1021=716%:%
-%:%1022=717%:%
-%:%1023=718%:%
-%:%1026=719%:%
-%:%1027=720%:%
-%:%1028=720%:%
-%:%1029=721%:%
-%:%1030=722%:%
-%:%1031=723%:%
-%:%1032=724%:%
-%:%1035=725%:%
-%:%1036=726%:%
-%:%1037=726%:%
-%:%1038=727%:%
-%:%1039=728%:%
-%:%1040=729%:%
-%:%1041=730%:%
-%:%1044=731%:%
-%:%1047=732%:%
-%:%1048=733%:%
-%:%1049=733%:%
-%:%1050=734%:%
-%:%1053=737%:%
-%:%1054=738%:%
-%:%1055=739%:%
-%:%1056=739%:%
-%:%1057=740%:%
-%:%1060=743%:%
-%:%1063=744%:%
-%:%1068=745%:%
\ No newline at end of file