(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. SPDX-License-Identifier: MIT *) theory Shallow_Micro_Rust imports Basic_Case_Expression Bool_Type Bool_Type_Lemmas Core_Expression Core_Expression_Lemmas Core_Syntax Eval Global_Store Micro_Rust Micro_Rust_Shallow_Embedding Numeric_Types Numeric_Types_Lemmas Option_Type Pullback Range_Type Result_Type Rust_Iterator Rust_Iterator_Lemmas Prompts_And_Responses SSA Tuple begin end