Update Lean printer to new infrastructure

hax-lib/proof-libs/lean/Lib.lean

@@ -220,6 +220,8 @@ instance {β} : Coe (α -> i32 -> β) (α -> Nat -> β) where
 instance : OfNat (Result Nat) n where
   ofNat := pure (n)
 
+instance {α n} [i: OfNat α n] : OfNat (Result α) n where
+  ofNat := pure (i.ofNat)
 
 /-
 
@@ -815,7 +817,9 @@ end Fold
 Rust arrays, are represented as Lean `Vector` (Lean Arrays of known size)
 
 -/
-section Array
+section RustArray
+
+abbrev RustArray := Vector
 
 inductive array_TryFromSliceError where
   | array_TryFromSliceError
@@ -847,7 +851,7 @@ def convert_TryInto_try_into {α n} (a: Array α) :
        .err .array_TryFromSliceError
      )
 
-end Array
+end RustArray
 
 /-
 
@@ -1038,6 +1042,8 @@ Rust vectors are represented as Lean Arrays (variable size)
 -/
 section RustVectors
 
+abbrev RustVector := Array
+
 def alloc_Global : Type := Unit
 def vec_Vec (α: Type) (_Allocator:Type) : Type := Array α
 

rust-engine/src/backends.rs

@@ -51,7 +51,7 @@ pub trait Backend {
 
     /// The AST phases to apply before printing.
     ///
-    /// Backends can override this to add transformations.  
+    /// Backends can override this to add transformations.
     /// The default is an empty list (no transformations).
     fn phases(&self) -> Vec<Box<dyn crate::phase::Phase>> {
         vec![]
@@ -115,10 +115,15 @@ mod prelude {
     //! Importing this prelude saves repetitive `use` lists in per-backend
     //! modules without forcing these names on downstream users.
     pub use super::Backend;
+    pub use crate::ast::identifiers::*;
+    pub use crate::ast::literals::*;
+    pub use crate::ast::resugared::*;
     pub use crate::ast::*;
     pub use crate::printer::*;
+    pub use crate::symbol::Symbol;
     pub use hax_rust_engine_macros::prepend_associated_functions_with;
     pub use pretty::DocAllocator;
+    pub use pretty::DocBuilder;
     pub use pretty::Pretty;
     pub use pretty_ast::install_pretty_helpers;
 }