\begin{lexlean}{Calculator}
\useglossary{lexlean.std.bool@1.1.0}
\useglossary{lexlean.std.nat@1.1.0}
\title{Boolean}
\begin{semanticmodule}
\semanticdata{{"declarations":[{"constructors":[{"fields":[],"name":"Add"},{"fields":[],"name":"Subtract"},{"fields":[],"name":"Multiply"},{"fields":[],"name":"Divide"}],"kind":"inductive","name":"Operation","parameters":[],"type_parameters":[]},{"constructors":[{"fields":[],"name":"DivisionByZero"},{"fields":[],"name":"Overflow"}],"kind":"inductive","name":"CalculatorError","parameters":[],"type_parameters":[]},{"constructors":[{"fields":[],"name":"MalformedRequest"},{"fields":[],"name":"UnsupportedVersion"},{"fields":[],"name":"UnknownOperation"}],"kind":"inductive","name":"ProtocolError","parameters":[],"type_parameters":[]},{"fields":[{"name":"label","type":{"kind":"string"}},{"name":"requestName","type":{"kind":"string"}},{"name":"rustVariant","type":{"kind":"string"}},{"name":"discriminant","type":{"kind":"uint8"}}],"kind":"structure","name":"ViewOperation","parameters":[],"type_parameters":[]},{"fields":[{"name":"title","type":{"kind":"string"}},{"name":"heading","type":{"kind":"string"}},{"name":"leftLabel","type":{"kind":"string"}},{"name":"rightLabel","type":{"kind":"string"}},{"name":"operationLabel","type":{"kind":"string"}},{"name":"submitLabel","type":{"kind":"string"}},{"name":"inputError","type":{"kind":"string"}},{"name":"divisionError","type":{"kind":"string"}},{"name":"overflowError","type":{"kind":"string"}},{"name":"livePolite","type":{"kind":"bool"}},{"name":"retainFocus","type":{"kind":"bool"}},{"name":"submitOnEnter","type":{"kind":"bool"}},{"name":"hologramIntent","type":{"kind":"bool"}},{"name":"pagesAdapter","type":{"kind":"bool"}},{"name":"operations","type":{"element":{"arguments":[],"kind":"named","member":{"name":"ViewOperation"}},"kind":"list"}},{"name":"initialOperation","type":{"kind":"uint8"}}],"kind":"structure","name":"CalculatorView","parameters":[],"type_parameters":[]},{"fields":[{"name":"operation","type":{"arguments":[],"kind":"named","member":{"name":"Operation"}}},{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"kind":"structure","name":"Request","parameters":[],"type_parameters":[]},{"constructors":[{"fields":[],"name":"AsciiSignedI64"}],"kind":"inductive","name":"InputGrammar","parameters":[],"type_parameters":[]},{"constructors":[{"fields":[],"name":"Submit"},{"fields":[],"name":"Enter"}],"kind":"inductive","name":"ViewAction","parameters":[],"type_parameters":[]},{"constructors":[{"fields":[],"name":"Polite"}],"kind":"inductive","name":"LiveMode","parameters":[],"type_parameters":[]},{"constructors":[{"fields":[],"name":"Compact"},{"fields":[],"name":"HighContrast"},{"fields":[],"name":"SystemSans"}],"kind":"inductive","name":"StyleToken","parameters":[],"type_parameters":[]},{"constructors":[{"fields":[],"name":"HologramPortable"},{"fields":[],"name":"GithubPages"}],"kind":"inductive","name":"PresentationTarget","parameters":[],"type_parameters":[]},{"fields":[{"name":"request","type":{"kind":"bytes"}},{"name":"response","type":{"kind":"bytes"}}],"kind":"structure","name":"AcceptanceVector","parameters":[],"type_parameters":[]},{"fields":[{"name":"name","type":{"kind":"string"}},{"name":"cargoName","type":{"kind":"string"}},{"name":"cargoVersion","type":{"kind":"string"}},{"name":"cargoDescription","type":{"kind":"string"}},{"name":"cargoRepository","type":{"kind":"string"}},{"name":"cargoHomepage","type":{"kind":"string"}},{"name":"libraryRoots","type":{"element":{"kind":"string"},"kind":"list"}},{"name":"operationType","type":{"kind":"string"}},{"name":"errorType","type":{"kind":"string"}},{"name":"functionName","type":{"kind":"string"}},{"name":"acceptanceVectors","type":{"element":{"arguments":[],"kind":"named","member":{"name":"AcceptanceVector"}},"kind":"list"}},{"name":"entryRoot","type":{"kind":"string"}},{"name":"coreContract","type":{"kind":"string"}},{"name":"requestMaximum","type":{"kind":"uint32"}},{"name":"responseMaximum","type":{"kind":"uint32"}},{"name":"guestAllocationMaximum","type":{"kind":"uint32"}},{"name":"capabilitiesEmpty","type":{"kind":"bool"}},{"name":"fatArchive","type":{"kind":"bool"}},{"name":"primaryLayer","type":{"kind":"uint8"}},{"name":"viewLayer","type":{"kind":"uint8"}},{"name":"view","type":{"arguments":[],"kind":"named","member":{"name":"CalculatorView"}}},{"name":"inputGrammar","type":{"arguments":[],"kind":"named","member":{"name":"InputGrammar"}}},{"name":"liveMode","type":{"arguments":[],"kind":"named","member":{"name":"LiveMode"}}},{"name":"layout","type":{"arguments":[],"kind":"named","member":{"name":"StyleToken"}}},{"name":"color","type":{"arguments":[],"kind":"named","member":{"name":"StyleToken"}}},{"name":"typography","type":{"arguments":[],"kind":"named","member":{"name":"StyleToken"}}},{"name":"actions","type":{"element":{"arguments":[],"kind":"named","member":{"name":"ViewAction"}},"kind":"list"}},{"name":"targets","type":{"element":{"arguments":[],"kind":"named","member":{"name":"PresentationTarget"}},"kind":"list"}}],"kind":"structure","name":"CalculatorApplication","parameters":[],"type_parameters":[]},{"axioms":[],"body":{"branches":[{"binders":[],"body":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"CalculatorError.Overflow"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]},"constructor":{"name":"Option.none"}},{"binders":["value"],"body":{"arguments":[{"kind":"var","name":"value"}],"constructor":{"name":"Result.ok"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]},"constructor":{"name":"Option.some"}}],"kind":"match","scrutinee":{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"kind":"primitive","operation":"checked_add","result":{"kind":"option","value":{"kind":"int64"}}}},"constructor":{"name":"Operation.Add"}},{"binders":[],"body":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"CalculatorError.Overflow"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]},"constructor":{"name":"Option.none"}},{"binders":["value"],"body":{"arguments":[{"kind":"var","name":"value"}],"constructor":{"name":"Result.ok"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]},"constructor":{"name":"Option.some"}}],"kind":"match","scrutinee":{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"kind":"primitive","operation":"checked_subtract","result":{"kind":"option","value":{"kind":"int64"}}}},"constructor":{"name":"Operation.Subtract"}},{"binders":[],"body":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"CalculatorError.Overflow"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]},"constructor":{"name":"Option.none"}},{"binders":["value"],"body":{"arguments":[{"kind":"var","name":"value"}],"constructor":{"name":"Result.ok"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]},"constructor":{"name":"Option.some"}}],"kind":"match","scrutinee":{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"kind":"primitive","operation":"checked_multiply","result":{"kind":"option","value":{"kind":"int64"}}}},"constructor":{"name":"Operation.Multiply"}},{"binders":[],"body":{"condition":{"arguments":[{"kind":"var","name":"right"},{"kind":"integer","representation":"int64","value":"0"}],"kind":"primitive","operation":"equal","result":{"kind":"bool"}},"else_value":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"CalculatorError.Overflow"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]},"constructor":{"name":"Option.none"}},{"binders":["value"],"body":{"arguments":[{"kind":"var","name":"value"}],"constructor":{"name":"Result.ok"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]},"constructor":{"name":"Option.some"}}],"kind":"match","scrutinee":{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"kind":"primitive","operation":"checked_quotient","result":{"kind":"option","value":{"kind":"int64"}}}},"kind":"if","then_value":{"arguments":[{"arguments":[],"constructor":{"name":"CalculatorError.DivisionByZero"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]}},"constructor":{"name":"Operation.Divide"}}],"kind":"match","scrutinee":{"kind":"var","name":"operation"}},"kind":"definition","name":"calculate","parameters":[{"name":"operation","type":{"arguments":[],"kind":"named","member":{"name":"Operation"}}},{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}},"kind":"result","ok":{"kind":"int64"}}},{"body":{"fields":[{"field":"title","value":{"kind":"string","value":"Calculator"}},{"field":"heading","value":{"kind":"string","value":"Calculator"}},{"field":"leftLabel","value":{"kind":"string","value":"Left operand"}},{"field":"rightLabel","value":{"kind":"string","value":"Right operand"}},{"field":"operationLabel","value":{"kind":"string","value":"Operation"}},{"field":"submitLabel","value":{"kind":"string","value":"Calculate"}},{"field":"inputError","value":{"kind":"string","value":"Enter a signed 64-bit integer."}},{"field":"divisionError","value":{"kind":"string","value":"Division by zero."}},{"field":"overflowError","value":{"kind":"string","value":"Arithmetic overflow."}},{"field":"livePolite","value":{"kind":"bool","value":true}},{"field":"retainFocus","value":{"kind":"bool","value":true}},{"field":"submitOnEnter","value":{"kind":"bool","value":true}},{"field":"hologramIntent","value":{"kind":"bool","value":true}},{"field":"pagesAdapter","value":{"kind":"bool","value":true}},{"field":"operations","value":{"head":{"fields":[{"field":"label","value":{"kind":"string","value":"Add"}},{"field":"requestName","value":{"kind":"string","value":"add"}},{"field":"rustVariant","value":{"kind":"string","value":"Add"}},{"field":"discriminant","value":{"kind":"integer","representation":"uint8","value":"0"}}],"kind":"record","type":{"name":"ViewOperation"}},"kind":"cons","tail":{"head":{"fields":[{"field":"label","value":{"kind":"string","value":"Subtract"}},{"field":"requestName","value":{"kind":"string","value":"subtract"}},{"field":"rustVariant","value":{"kind":"string","value":"Subtract"}},{"field":"discriminant","value":{"kind":"integer","representation":"uint8","value":"1"}}],"kind":"record","type":{"name":"ViewOperation"}},"kind":"cons","tail":{"head":{"fields":[{"field":"label","value":{"kind":"string","value":"Multiply"}},{"field":"requestName","value":{"kind":"string","value":"multiply"}},{"field":"rustVariant","value":{"kind":"string","value":"Multiply"}},{"field":"discriminant","value":{"kind":"integer","representation":"uint8","value":"2"}}],"kind":"record","type":{"name":"ViewOperation"}},"kind":"cons","tail":{"head":{"fields":[{"field":"label","value":{"kind":"string","value":"Divide"}},{"field":"requestName","value":{"kind":"string","value":"divide"}},{"field":"rustVariant","value":{"kind":"string","value":"Divide"}},{"field":"discriminant","value":{"kind":"integer","representation":"uint8","value":"3"}}],"kind":"record","type":{"name":"ViewOperation"}},"kind":"cons","tail":{"element":{"arguments":[],"kind":"named","member":{"name":"ViewOperation"}},"kind":"nil"}}}}}},{"field":"initialOperation","value":{"kind":"integer","representation":"uint8","value":"0"}}],"kind":"record","type":{"name":"CalculatorView"}},"kind":"definition","name":"calculatorView","parameters":[],"result":{"arguments":[],"kind":"named","member":{"name":"CalculatorView"}}},{"axioms":[],"body":{"kind":"eq","left":{"arguments":[{"kind":"var","name":"operation"},{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"function":{"name":"calculate"},"kind":"call"},"right":{"arguments":[{"kind":"var","name":"operation"},{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"function":{"name":"calculate"},"kind":"call"}},"kind":"definition","name":"calculationCorrect","parameters":[{"name":"operation","type":{"arguments":[],"kind":"named","member":{"name":"Operation"}}},{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"result":{"kind":"prop"}},{"axioms":[],"kind":"theorem","name":"calculate_correct","parameters":[{"name":"operation","type":{"arguments":[],"kind":"named","member":{"name":"Operation"}}},{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"proof":{"kind":"reflexivity"},"statement":{"arguments":[{"kind":"var","name":"operation"},{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"function":{"name":"calculationCorrect"},"kind":"call"}},{"axioms":[],"body":{"condition":{"arguments":[{"kind":"var","name":"value"},{"kind":"string","value":"add"}],"kind":"primitive","operation":"equal","result":{"kind":"bool"}},"else_value":{"condition":{"arguments":[{"kind":"var","name":"value"},{"kind":"string","value":"subtract"}],"kind":"primitive","operation":"equal","result":{"kind":"bool"}},"else_value":{"condition":{"arguments":[{"kind":"var","name":"value"},{"kind":"string","value":"multiply"}],"kind":"primitive","operation":"equal","result":{"kind":"bool"}},"else_value":{"condition":{"arguments":[{"kind":"var","name":"value"},{"kind":"string","value":"divide"}],"kind":"primitive","operation":"equal","result":{"kind":"bool"}},"else_value":{"arguments":[{"arguments":[],"constructor":{"name":"ProtocolError.UnknownOperation"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Operation"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"kind":"if","then_value":{"arguments":[{"arguments":[],"constructor":{"name":"Operation.Divide"},"kind":"constructor"}],"constructor":{"name":"Result.ok"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Operation"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]}},"kind":"if","then_value":{"arguments":[{"arguments":[],"constructor":{"name":"Operation.Multiply"},"kind":"constructor"}],"constructor":{"name":"Result.ok"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Operation"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]}},"kind":"if","then_value":{"arguments":[{"arguments":[],"constructor":{"name":"Operation.Subtract"},"kind":"constructor"}],"constructor":{"name":"Result.ok"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Operation"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]}},"kind":"if","then_value":{"arguments":[{"arguments":[],"constructor":{"name":"Operation.Add"},"kind":"constructor"}],"constructor":{"name":"Result.ok"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Operation"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]}},"kind":"definition","name":"parseOperation","parameters":[{"name":"value","type":{"kind":"string"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}},"kind":"result","ok":{"arguments":[],"kind":"named","member":{"name":"Operation"}}}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"ProtocolError.MalformedRequest"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Request"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"constructor":{"name":"Option.none"}},{"binders":["right"],"body":{"arguments":[{"fields":[{"field":"operation","value":{"kind":"var","name":"operation"}},{"field":"left","value":{"kind":"var","name":"left"}},{"field":"right","value":{"kind":"var","name":"right"}}],"kind":"record","type":{"name":"Request"}}],"constructor":{"name":"Result.ok"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Request"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"constructor":{"name":"Option.some"}}],"kind":"match","scrutinee":{"arguments":[{"kind":"var","name":"rightText"}],"kind":"primitive","operation":"parse_decimal","result":{"kind":"option","value":{"kind":"int64"}}}},"kind":"definition","name":"decodeRight","parameters":[{"name":"operation","type":{"arguments":[],"kind":"named","member":{"name":"Operation"}}},{"name":"left","type":{"kind":"int64"}},{"name":"rightText","type":{"kind":"string"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}},"kind":"result","ok":{"arguments":[],"kind":"named","member":{"name":"Request"}}}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"ProtocolError.MalformedRequest"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Request"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"constructor":{"name":"Option.none"}},{"binders":["left"],"body":{"arguments":[{"kind":"var","name":"operation"},{"kind":"var","name":"left"},{"kind":"var","name":"rightText"}],"function":{"name":"decodeRight"},"kind":"call"},"constructor":{"name":"Option.some"}}],"kind":"match","scrutinee":{"arguments":[{"kind":"var","name":"leftText"}],"kind":"primitive","operation":"parse_decimal","result":{"kind":"option","value":{"kind":"int64"}}}},"kind":"definition","name":"decodeLeft","parameters":[{"name":"operation","type":{"arguments":[],"kind":"named","member":{"name":"Operation"}}},{"name":"leftText","type":{"kind":"string"}},{"name":"rightText","type":{"kind":"string"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}},"kind":"result","ok":{"arguments":[],"kind":"named","member":{"name":"Request"}}}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"condition":{"arguments":[{"kind":"var","name":"version"},{"kind":"string","value":"1"}],"kind":"primitive","operation":"equal","result":{"kind":"bool"}},"else_value":{"arguments":[{"arguments":[],"constructor":{"name":"ProtocolError.UnsupportedVersion"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Request"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"kind":"if","then_value":{"branches":[{"binders":["error"],"body":{"arguments":[{"kind":"var","name":"error"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Request"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"constructor":{"name":"Result.error"}},{"binders":["operation"],"body":{"arguments":[{"kind":"var","name":"operation"},{"kind":"var","name":"leftText"},{"kind":"var","name":"rightText"}],"function":{"name":"decodeLeft"},"kind":"call"},"constructor":{"name":"Result.ok"}}],"kind":"match","scrutinee":{"arguments":[{"kind":"var","name":"operationText"}],"function":{"name":"parseOperation"},"kind":"call"}}},"kind":"definition","name":"decodeComplete","parameters":[{"name":"version","type":{"kind":"string"}},{"name":"operationText","type":{"kind":"string"}},{"name":"leftText","type":{"kind":"string"}},{"name":"rightText","type":{"kind":"string"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}},"kind":"result","ok":{"arguments":[],"kind":"named","member":{"name":"Request"}}}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"branches":[{"binders":[],"body":{"arguments":[{"kind":"var","name":"version"},{"kind":"var","name":"operationText"},{"kind":"var","name":"leftText"},{"kind":"var","name":"rightText"}],"function":{"name":"decodeComplete"},"kind":"call"},"constructor":{"name":"List.nil"}},{"binders":["extra","rest"],"body":{"arguments":[{"arguments":[],"constructor":{"name":"ProtocolError.MalformedRequest"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Request"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"constructor":{"name":"List.cons"}}],"kind":"match","scrutinee":{"kind":"var","name":"values"}},"kind":"definition","name":"decodeTail4","parameters":[{"name":"version","type":{"kind":"string"}},{"name":"operationText","type":{"kind":"string"}},{"name":"leftText","type":{"kind":"string"}},{"name":"rightText","type":{"kind":"string"}},{"name":"values","type":{"element":{"kind":"string"},"kind":"list"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}},"kind":"result","ok":{"arguments":[],"kind":"named","member":{"name":"Request"}}}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"ProtocolError.MalformedRequest"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Request"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"constructor":{"name":"List.nil"}},{"binders":["rightText","rest"],"body":{"arguments":[{"kind":"var","name":"version"},{"kind":"var","name":"operationText"},{"kind":"var","name":"leftText"},{"kind":"var","name":"rightText"},{"kind":"var","name":"rest"}],"function":{"name":"decodeTail4"},"kind":"call"},"constructor":{"name":"List.cons"}}],"kind":"match","scrutinee":{"kind":"var","name":"values"}},"kind":"definition","name":"decodeTail3","parameters":[{"name":"version","type":{"kind":"string"}},{"name":"operationText","type":{"kind":"string"}},{"name":"leftText","type":{"kind":"string"}},{"name":"values","type":{"element":{"kind":"string"},"kind":"list"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}},"kind":"result","ok":{"arguments":[],"kind":"named","member":{"name":"Request"}}}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"ProtocolError.MalformedRequest"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Request"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"constructor":{"name":"List.nil"}},{"binders":["leftText","rest"],"body":{"arguments":[{"kind":"var","name":"version"},{"kind":"var","name":"operationText"},{"kind":"var","name":"leftText"},{"kind":"var","name":"rest"}],"function":{"name":"decodeTail3"},"kind":"call"},"constructor":{"name":"List.cons"}}],"kind":"match","scrutinee":{"kind":"var","name":"values"}},"kind":"definition","name":"decodeTail2","parameters":[{"name":"version","type":{"kind":"string"}},{"name":"operationText","type":{"kind":"string"}},{"name":"values","type":{"element":{"kind":"string"},"kind":"list"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}},"kind":"result","ok":{"arguments":[],"kind":"named","member":{"name":"Request"}}}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"ProtocolError.MalformedRequest"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Request"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"constructor":{"name":"List.nil"}},{"binders":["operationText","rest"],"body":{"arguments":[{"kind":"var","name":"version"},{"kind":"var","name":"operationText"},{"kind":"var","name":"rest"}],"function":{"name":"decodeTail2"},"kind":"call"},"constructor":{"name":"List.cons"}}],"kind":"match","scrutinee":{"kind":"var","name":"values"}},"kind":"definition","name":"decodeTail1","parameters":[{"name":"version","type":{"kind":"string"}},{"name":"values","type":{"element":{"kind":"string"},"kind":"list"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}},"kind":"result","ok":{"arguments":[],"kind":"named","member":{"name":"Request"}}}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"ProtocolError.MalformedRequest"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Request"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"constructor":{"name":"List.nil"}},{"binders":["version","rest"],"body":{"arguments":[{"kind":"var","name":"version"},{"kind":"var","name":"rest"}],"function":{"name":"decodeTail1"},"kind":"call"},"constructor":{"name":"List.cons"}}],"kind":"match","scrutinee":{"kind":"var","name":"values"}},"kind":"definition","name":"decodeFields","parameters":[{"name":"values","type":{"element":{"kind":"string"},"kind":"list"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}},"kind":"result","ok":{"arguments":[],"kind":"named","member":{"name":"Request"}}}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"ProtocolError.MalformedRequest"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"arguments":[],"kind":"named","member":{"name":"Request"}},{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}]},"constructor":{"name":"Option.none"}},{"binders":["fields"],"body":{"arguments":[{"kind":"var","name":"fields"}],"function":{"name":"decodeFields"},"kind":"call"},"constructor":{"name":"Option.some"}}],"kind":"match","scrutinee":{"arguments":[{"kind":"var","name":"value"},{"kind":"string","value":"\t"},{"kind":"integer","representation":"uint32","value":"4"}],"kind":"primitive","operation":"split_exact","result":{"kind":"option","value":{"element":{"kind":"string"},"kind":"list"}}}},"kind":"definition","name":"decodeRequest","parameters":[{"name":"value","type":{"kind":"string"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}},"kind":"result","ok":{"arguments":[],"kind":"named","member":{"name":"Request"}}}},{"axioms":[],"body":{"branches":[{"binders":[],"body":{"kind":"string","value":"1\terror\tmalformed-request"},"constructor":{"name":"ProtocolError.MalformedRequest"}},{"binders":[],"body":{"kind":"string","value":"1\terror\tunsupported-version"},"constructor":{"name":"ProtocolError.UnsupportedVersion"}},{"binders":[],"body":{"kind":"string","value":"1\terror\tunknown-operation"},"constructor":{"name":"ProtocolError.UnknownOperation"}}],"kind":"match","scrutinee":{"kind":"var","name":"error"}},"kind":"definition","name":"encodeProtocolError","parameters":[{"name":"error","type":{"arguments":[],"kind":"named","member":{"name":"ProtocolError"}}}],"result":{"kind":"string"}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"branches":[{"binders":["error"],"body":{"branches":[{"binders":[],"body":{"kind":"string","value":"1\terror\tdivision-by-zero"},"constructor":{"name":"CalculatorError.DivisionByZero"}},{"binders":[],"body":{"kind":"string","value":"1\terror\toverflow"},"constructor":{"name":"CalculatorError.Overflow"}}],"kind":"match","scrutinee":{"kind":"var","name":"error"}},"constructor":{"name":"Result.error"}},{"binders":["result"],"body":{"arguments":[{"head":{"kind":"string","value":"1\tok\t"},"kind":"cons","tail":{"head":{"arguments":[{"kind":"var","name":"result"}],"kind":"primitive","operation":"format_decimal","result":{"kind":"string"}},"kind":"cons","tail":{"element":{"kind":"string"},"kind":"nil"}}},{"kind":"string","value":""}],"kind":"primitive","operation":"join","result":{"kind":"string"}},"constructor":{"name":"Result.ok"}}],"kind":"match","scrutinee":{"kind":"var","name":"value"}},"kind":"definition","name":"encodeCalculationResult","parameters":[{"name":"value","type":{"error":{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}},"kind":"result","ok":{"kind":"int64"}}}],"result":{"kind":"string"}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"branches":[{"binders":["error"],"body":{"arguments":[{"kind":"var","name":"error"}],"function":{"name":"encodeProtocolError"},"kind":"call"},"constructor":{"name":"Result.error"}},{"binders":["request"],"body":{"arguments":[{"arguments":[{"field":"operation","kind":"project","value":{"kind":"var","name":"request"}},{"field":"left","kind":"project","value":{"kind":"var","name":"request"}},{"field":"right","kind":"project","value":{"kind":"var","name":"request"}}],"function":{"name":"calculate"},"kind":"call"}],"function":{"name":"encodeCalculationResult"},"kind":"call"},"constructor":{"name":"Result.ok"}}],"kind":"match","scrutinee":{"arguments":[{"kind":"var","name":"value"}],"function":{"name":"decodeRequest"},"kind":"call"}},"kind":"definition","name":"dispatchString","parameters":[{"name":"value","type":{"kind":"string"}}],"result":{"kind":"string"}},{"axioms":["Classical.choice","Quot.sound","propext"],"body":{"branches":[{"binders":[],"body":{"arguments":[{"kind":"string","value":"1\terror\tmalformed-request"}],"kind":"primitive","operation":"utf8_encode","result":{"kind":"bytes"}},"constructor":{"name":"Option.none"}},{"binders":["text"],"body":{"arguments":[{"arguments":[{"kind":"var","name":"text"}],"function":{"name":"dispatchString"},"kind":"call"}],"kind":"primitive","operation":"utf8_encode","result":{"kind":"bytes"}},"constructor":{"name":"Option.some"}}],"kind":"match","scrutinee":{"arguments":[{"kind":"var","name":"value"}],"kind":"primitive","operation":"utf8_decode","result":{"kind":"option","value":{"kind":"string"}}}},"kind":"definition","name":"dispatchBytes","parameters":[{"name":"value","type":{"kind":"bytes"}}],"result":{"kind":"bytes"}},{"body":{"fields":[{"field":"name","value":{"kind":"string","value":"Calculator"}},{"field":"cargoName","value":{"kind":"string","value":"prism-calculator"}},{"field":"cargoVersion","value":{"kind":"string","value":"0.1.0"}},{"field":"cargoDescription","value":{"kind":"string","value":"A Lean-verified, Prism-generated checked i64 calculator."}},{"field":"cargoRepository","value":{"kind":"string","value":"https://github.com/UOR-Foundation/PrismPM"}},{"field":"cargoHomepage","value":{"kind":"string","value":"https://uor-foundation.github.io/calculator-example/"}},{"field":"libraryRoots","value":{"head":{"kind":"string","value":"PrismCalculator.Calculator.calculate"},"kind":"cons","tail":{"head":{"kind":"string","value":"PrismCalculator.Calculator.dispatchBytes"},"kind":"cons","tail":{"element":{"kind":"string"},"kind":"nil"}}}},{"field":"operationType","value":{"kind":"string","value":"Operation"}},{"field":"errorType","value":{"kind":"string","value":"CalculatorError"}},{"field":"functionName","value":{"kind":"string","value":"calculate"}},{"field":"acceptanceVectors","value":{"head":{"fields":[{"field":"request","value":{"hex":"310961646409300930","kind":"bytes"}},{"field":"response","value":{"hex":"31096f6b0930","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"3109616464093230093232","kind":"bytes"}},{"field":"response","value":{"hex":"31096f6b093432","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"310961646409393232333337323033363835343737353830370930","kind":"bytes"}},{"field":"response","value":{"hex":"31096f6b0939323233333732303336383534373735383037","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"310961646409393232333337323033363835343737353830370931","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096f766572666c6f77","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"3109616464092d39323233333732303336383534373735383038092d31","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096f766572666c6f77","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"31097375627472616374092d370935","kind":"bytes"}},{"field":"response","value":{"hex":"31096f6b092d3132","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"31097375627472616374092d393232333337323033363835343737353830380931","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096f766572666c6f77","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"310973756274726163740939323233333732303336383534373735383037092d31","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096f766572666c6f77","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"31096d756c7469706c79092d360937","kind":"bytes"}},{"field":"response","value":{"hex":"31096f6b092d3432","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"31096d756c7469706c7909393232333337323033363835343737353830370932","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096f766572666c6f77","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"31096d756c7469706c79092d39323233333732303336383534373735383038092d31","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096f766572666c6f77","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"3109646976696465092d370933","kind":"bytes"}},{"field":"response","value":{"hex":"31096f6b092d32","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"31096469766964650937092d33","kind":"bytes"}},{"field":"response","value":{"hex":"31096f6b092d32","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"310964697669646509310930","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096469766973696f6e2d62792d7a65726f","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"3109646976696465092d39323233333732303336383534373735383038092d31","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096f766572666c6f77","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096d616c666f726d65642d72657175657374","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"320961646409310932","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f7209756e737570706f727465642d76657273696f6e","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"31096d6f6409310932","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f7209756e6b6e6f776e2d6f7065726174696f6e","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"31096164640930310932","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096d616c666f726d65642d72657175657374","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"3109616464092b310932","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096d616c666f726d65642d72657175657374","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"31096164640931","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096d616c666f726d65642d72657175657374","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"head":{"fields":[{"field":"request","value":{"hex":"ff","kind":"bytes"}},{"field":"response","value":{"hex":"31096572726f72096d616c666f726d65642d72657175657374","kind":"bytes"}}],"kind":"record","type":{"name":"AcceptanceVector"}},"kind":"cons","tail":{"element":{"arguments":[],"kind":"named","member":{"name":"AcceptanceVector"}},"kind":"nil"}}}}}}}}}}}}}}}}}}}}}}}},{"field":"entryRoot","value":{"kind":"string","value":"PrismCalculator.Calculator.dispatchBytes"}},{"field":"coreContract","value":{"kind":"string","value":"hologram:guest/core-wasm@1"}},{"field":"requestMaximum","value":{"kind":"integer","representation":"uint32","value":"52"}},{"field":"responseMaximum","value":{"kind":"integer","representation":"uint32","value":"27"}},{"field":"guestAllocationMaximum","value":{"kind":"integer","representation":"uint32","value":"65536"}},{"field":"capabilitiesEmpty","value":{"kind":"bool","value":true}},{"field":"fatArchive","value":{"kind":"bool","value":true}},{"field":"primaryLayer","value":{"kind":"integer","representation":"uint8","value":"0"}},{"field":"viewLayer","value":{"kind":"integer","representation":"uint8","value":"1"}},{"field":"view","value":{"arguments":[],"function":{"name":"calculatorView"},"kind":"call"}},{"field":"inputGrammar","value":{"arguments":[],"constructor":{"name":"InputGrammar.AsciiSignedI64"},"kind":"constructor"}},{"field":"liveMode","value":{"arguments":[],"constructor":{"name":"LiveMode.Polite"},"kind":"constructor"}},{"field":"layout","value":{"arguments":[],"constructor":{"name":"StyleToken.Compact"},"kind":"constructor"}},{"field":"color","value":{"arguments":[],"constructor":{"name":"StyleToken.HighContrast"},"kind":"constructor"}},{"field":"typography","value":{"arguments":[],"constructor":{"name":"StyleToken.SystemSans"},"kind":"constructor"}},{"field":"actions","value":{"head":{"arguments":[],"constructor":{"name":"ViewAction.Submit"},"kind":"constructor"},"kind":"cons","tail":{"head":{"arguments":[],"constructor":{"name":"ViewAction.Enter"},"kind":"constructor"},"kind":"cons","tail":{"element":{"arguments":[],"kind":"named","member":{"name":"ViewAction"}},"kind":"nil"}}}},{"field":"targets","value":{"head":{"arguments":[],"constructor":{"name":"PresentationTarget.HologramPortable"},"kind":"constructor"},"kind":"cons","tail":{"head":{"arguments":[],"constructor":{"name":"PresentationTarget.GithubPages"},"kind":"constructor"},"kind":"cons","tail":{"element":{"arguments":[],"kind":"named","member":{"name":"PresentationTarget"}},"kind":"nil"}}}}],"kind":"record","type":{"name":"CalculatorApplication"}},"kind":"definition","name":"calculatorApplication","parameters":[],"result":{"arguments":[],"kind":"named","member":{"name":"CalculatorApplication"}}},{"axioms":[],"body":{"branches":[{"binders":[],"body":{"arguments":[{"arguments":[],"constructor":{"name":"CalculatorError.Overflow"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]},"constructor":{"name":"Option.none"}},{"binders":["result"],"body":{"arguments":[{"kind":"var","name":"result"}],"constructor":{"name":"Result.ok"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]},"constructor":{"name":"Option.some"}}],"kind":"match","scrutinee":{"kind":"var","name":"value"}},"kind":"definition","name":"checkedResult","parameters":[{"name":"value","type":{"kind":"option","value":{"kind":"int64"}}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}},"kind":"result","ok":{"kind":"int64"}}},{"axioms":[],"body":{"arguments":[{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"kind":"primitive","operation":"checked_add","result":{"kind":"option","value":{"kind":"int64"}}}],"function":{"name":"checkedResult"},"kind":"call"},"kind":"definition","name":"addExpected","parameters":[{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}},"kind":"result","ok":{"kind":"int64"}}},{"axioms":[],"body":{"arguments":[{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"kind":"primitive","operation":"checked_subtract","result":{"kind":"option","value":{"kind":"int64"}}}],"function":{"name":"checkedResult"},"kind":"call"},"kind":"definition","name":"subtractExpected","parameters":[{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}},"kind":"result","ok":{"kind":"int64"}}},{"axioms":[],"body":{"arguments":[{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"kind":"primitive","operation":"checked_multiply","result":{"kind":"option","value":{"kind":"int64"}}}],"function":{"name":"checkedResult"},"kind":"call"},"kind":"definition","name":"multiplyExpected","parameters":[{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}},"kind":"result","ok":{"kind":"int64"}}},{"axioms":[],"body":{"condition":{"arguments":[{"kind":"var","name":"right"},{"kind":"integer","representation":"int64","value":"0"}],"kind":"primitive","operation":"equal","result":{"kind":"bool"}},"else_value":{"arguments":[{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"kind":"primitive","operation":"checked_quotient","result":{"kind":"option","value":{"kind":"int64"}}}],"function":{"name":"checkedResult"},"kind":"call"},"kind":"if","then_value":{"arguments":[{"arguments":[],"constructor":{"name":"CalculatorError.DivisionByZero"},"kind":"constructor"}],"constructor":{"name":"Result.error"},"kind":"constructor","type_arguments":[{"kind":"int64"},{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}}]}},"kind":"definition","name":"divideExpected","parameters":[{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"result":{"error":{"arguments":[],"kind":"named","member":{"name":"CalculatorError"}},"kind":"result","ok":{"kind":"int64"}}},{"axioms":[],"kind":"theorem","name":"addCorrect","parameters":[{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"proof":{"kind":"reflexivity"},"statement":{"kind":"eq","left":{"arguments":[{"arguments":[],"constructor":{"name":"Operation.Add"},"kind":"constructor"},{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"function":{"name":"calculate"},"kind":"call"},"right":{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"function":{"name":"addExpected"},"kind":"call"}}},{"axioms":[],"kind":"theorem","name":"subtractCorrect","parameters":[{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"proof":{"kind":"reflexivity"},"statement":{"kind":"eq","left":{"arguments":[{"arguments":[],"constructor":{"name":"Operation.Subtract"},"kind":"constructor"},{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"function":{"name":"calculate"},"kind":"call"},"right":{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"function":{"name":"subtractExpected"},"kind":"call"}}},{"axioms":[],"kind":"theorem","name":"multiplyCorrect","parameters":[{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"proof":{"kind":"reflexivity"},"statement":{"kind":"eq","left":{"arguments":[{"arguments":[],"constructor":{"name":"Operation.Multiply"},"kind":"constructor"},{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"function":{"name":"calculate"},"kind":"call"},"right":{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"function":{"name":"multiplyExpected"},"kind":"call"}}},{"axioms":[],"kind":"theorem","name":"divideCorrect","parameters":[{"name":"left","type":{"kind":"int64"}},{"name":"right","type":{"kind":"int64"}}],"proof":{"kind":"reflexivity"},"statement":{"kind":"eq","left":{"arguments":[{"arguments":[],"constructor":{"name":"Operation.Divide"},"kind":"constructor"},{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"function":{"name":"calculate"},"kind":"call"},"right":{"arguments":[{"kind":"var","name":"left"},{"kind":"var","name":"right"}],"function":{"name":"divideExpected"},"kind":"call"}}}],"spec":"lexlean/semantic-module/1"}}
\end{semanticmodule}
\end{lexlean}