wip

formal-land · Oct 2, 2024 · e1c7503 · e1c7503
1 parent b801f78
commit e1c7503
Show file tree

Hide file tree

Showing 81 changed files with 6,507 additions and 7,288 deletions.
diff --git a/CoqOfRust/alloc/borrow.json b/CoqOfRust/alloc/borrow.json
@@ -828,39 +828,37 @@
               {
                 "name": "Borrowed",
                 "item": {
-                  "Tuple": {
-                    "tys": [
-                      {
-                        "type": "Application",
-                        "func": {
-                          "type": "Path",
-                          "path": [
-                            "&"
-                          ]
-                        },
-                        "consts": [],
-                        "tys": [
-                          {
-                            "type": "Var",
-                            "name": "B"
-                          }
+                  "type": "Tuple",
+                  "tys": [
+                    {
+                      "type": "Application",
+                      "func": {
+                        "type": "Path",
+                        "path": [
+                          "&"
                         ]
-                      }
-                    ]
-                  }
+                      },
+                      "consts": [],
+                      "tys": [
+                        {
+                          "type": "Var",
+                          "name": "B"
+                        }
+                      ]
+                    }
+                  ]
                 },
                 "discriminant": null
               },
               {
                 "name": "Owned",
                 "item": {
-                  "Tuple": {
-                    "tys": [
-                      {
-                        "type": "Associated"
-                      }
-                    ]
-                  }
+                  "type": "Tuple",
+                  "tys": [
+                    {
+                      "type": "Associated"
+                    }
+                  ]
                 },
                 "discriminant": null
               }

diff --git a/CoqOfRust/alloc/collections/btree/map/entry.json b/CoqOfRust/alloc/collections/btree/map/entry.json
@@ -38,78 +38,76 @@
                                 {
                                   "name": "Vacant",
                                   "item": {
-                                    "Tuple": {
-                                      "tys": [
-                                        {
-                                          "type": "Application",
-                                          "func": {
-                                            "type": "Path",
-                                            "path": [
-                                              "alloc",
-                                              "collections",
-                                              "btree",
-                                              "map",
-                                              "entry",
-                                              "VacantEntry"
-                                            ]
-                                          },
-                                          "consts": [],
-                                          "tys": [
-                                            {
-                                              "type": "Var",
-                                              "name": "K"
-                                            },
-                                            {
-                                              "type": "Var",
-                                              "name": "V"
-                                            },
-                                            {
-                                              "type": "Var",
-                                              "name": "A"
-                                            }
+                                    "type": "Tuple",
+                                    "tys": [
+                                      {
+                                        "type": "Application",
+                                        "func": {
+                                          "type": "Path",
+                                          "path": [
+                                            "alloc",
+                                            "collections",
+                                            "btree",
+                                            "map",
+                                            "entry",
+                                            "VacantEntry"
                                           ]
-                                        }
-                                      ]
-                                    }
+                                        },
+                                        "consts": [],
+                                        "tys": [
+                                          {
+                                            "type": "Var",
+                                            "name": "K"
+                                          },
+                                          {
+                                            "type": "Var",
+                                            "name": "V"
+                                          },
+                                          {
+                                            "type": "Var",
+                                            "name": "A"
+                                          }
+                                        ]
+                                      }
+                                    ]
                                   },
                                   "discriminant": null
                                 },
                                 {
                                   "name": "Occupied",
                                   "item": {
-                                    "Tuple": {
-                                      "tys": [
-                                        {
-                                          "type": "Application",
-                                          "func": {
-                                            "type": "Path",
-                                            "path": [
-                                              "alloc",
-                                              "collections",
-                                              "btree",
-                                              "map",
-                                              "entry",
-                                              "OccupiedEntry"
-                                            ]
-                                          },
-                                          "consts": [],
-                                          "tys": [
-                                            {
-                                              "type": "Var",
-                                              "name": "K"
-                                            },
-                                            {
-                                              "type": "Var",
-                                              "name": "V"
-                                            },
-                                            {
-                                              "type": "Var",
-                                              "name": "A"
-                                            }
+                                    "type": "Tuple",
+                                    "tys": [
+                                      {
+                                        "type": "Application",
+                                        "func": {
+                                          "type": "Path",
+                                          "path": [
+                                            "alloc",
+                                            "collections",
+                                            "btree",
+                                            "map",
+                                            "entry",
+                                            "OccupiedEntry"
                                           ]
-                                        }
-                                      ]
-                                    }
+                                        },
+                                        "consts": [],
+                                        "tys": [
+                                          {
+                                            "type": "Var",
+                                            "name": "K"
+                                          },
+                                          {
+                                            "type": "Var",
+                                            "name": "V"
+                                          },
+                                          {
+                                            "type": "Var",
+                                            "name": "A"
+                                          }
+                                        ]
+                                      }
+                                    ]
                                   },
                                   "discriminant": null
                                 }

diff --git a/CoqOfRust/alloc/collections/btree/merge_iter.json b/CoqOfRust/alloc/collections/btree/merge_iter.json
@@ -94,26 +94,24 @@
                           {
                             "name": "A",
                             "item": {
-                              "Tuple": {
-                                "tys": [
-                                  {
-                                    "type": "Associated"
-                                  }
-                                ]
-                              }
+                              "type": "Tuple",
+                              "tys": [
+                                {
+                                  "type": "Associated"
+                                }
+                              ]
                             },
                             "discriminant": null
                           },
                           {
                             "name": "B",
                             "item": {
-                              "Tuple": {
-                                "tys": [
-                                  {
-                                    "type": "Associated"
-                                  }
-                                ]
-                              }
+                              "type": "Tuple",
+                              "tys": [
+                                {
+                                  "type": "Associated"
+                                }
+                              ]
                             },
                             "discriminant": null
                           }