@@ -217,7 +217,10 @@ impl MemorySafetyProof {
217217 pub fn to_ats2_proof ( & self ) -> String {
218218 match self {
219219 MemorySafetyProof :: AllocProof { viewtype } => {
220- format ! ( "prval (pf_{} | p_{}) = alloc_{}" , viewtype, viewtype, viewtype)
220+ format ! (
221+ "prval (pf_{} | p_{}) = alloc_{}" ,
222+ viewtype, viewtype, viewtype
223+ )
221224 }
222225 MemorySafetyProof :: FreeProof { ptr_id } => {
223226 format ! ( "prval () = free_{}(pf_{}, p_{})" , ptr_id, ptr_id, ptr_id)
@@ -233,16 +236,10 @@ impl MemorySafetyProof {
233236 buffer_id,
234237 index_expr,
235238 } => {
236- format ! (
237- "prval () = lemma_bounds(pf_{}, {})" ,
238- buffer_id, index_expr
239- )
239+ format ! ( "prval () = lemma_bounds(pf_{}, {})" , buffer_id, index_expr)
240240 }
241241 MemorySafetyProof :: NullCheckProof { ptr_id } => {
242- format ! (
243- "prval () = opt_unsome(pf_{})" ,
244- ptr_id
245- )
242+ format ! ( "prval () = opt_unsome(pf_{})" , ptr_id)
246243 }
247244 }
248245 }
@@ -340,10 +337,7 @@ impl ATSModule {
340337 }
341338
342339 // Staload for C interop
343- out. push_str ( & format ! (
344- "staload \" {}_c.sats\" \n \n " ,
345- self . name
346- ) ) ;
340+ out. push_str ( & format ! ( "staload \" {}_c.sats\" \n \n " , self . name) ) ;
347341
348342 // Viewtype definitions
349343 for vt in & self . viewtypes {
@@ -381,10 +375,7 @@ fn generate_ats_function(func: &ATSFunction) -> String {
381375 } )
382376 . collect ( ) ;
383377
384- let ret = func
385- . return_type
386- . as_deref ( )
387- . unwrap_or ( "void" ) ;
378+ let ret = func. return_type . as_deref ( ) . unwrap_or ( "void" ) ;
388379
389380 out. push_str ( & format ! (
390381 "implement\n fun {}({}): {} = let\n " ,
0 commit comments