Merge pull request #500 from formal-land/gy@ExprToCoq

`expression::Expr::to_coq`

Author: InfiniteEchoes

CoqOfRust/examples/default/examples/rust_book/custom_types/structures.v

@@ -216,7 +216,7 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
     let* bottom_right :=
       let* α0 := M.read UnsupportedLiteral in
       let* α1 := M.read point in
-      M.alloc (M.struct_record_update (α1) [ ("x", α0) ]) in
+      M.alloc (M.struct_record_update α1 [ ("x", α0) ]) in
     let* _ :=
       let* _ :=
         let* α0 := M.get_function "std::io::stdio::_print" [] in

lib/src/coq.rs

@@ -89,7 +89,7 @@ pub(crate) enum Expression<'a> {
         name: Option<String>,
         is_monadic: bool,
         ty: Option<Rc<Expression<'a>>>,
-        value: Rc<Expression<'a>>,
+        init: Rc<Expression<'a>>,
         body: Rc<Expression<'a>>,
     },
     Match {
@@ -433,7 +433,7 @@ impl<'a> Expression<'a> {
                 name,
                 is_monadic,
                 ty,
-                value,
+                init,
                 body,
             } => {
                 // NOTE: The following variable is intended to bypass self-referencing issue for borrow checkers.
@@ -461,10 +461,10 @@ impl<'a> Expression<'a> {
                                 text(" :="),
                             ]),
                             line(),
-                            value.to_doc(false), // init
+                            init.to_doc(false),
                             text(" in"),
                         ]),
-                        line(),
+                        hardline(),
                         body.to_doc(false),
                     ]),
                 )