diff options
Diffstat (limited to 'tests/lean/misc-no_nested_borrows')
4 files changed, 43 insertions, 19 deletions
diff --git a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean index a20ee9fd..cf7783b2 100644 --- a/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean +++ b/tests/lean/misc-no_nested_borrows/NoNestedBorrows.lean @@ -5,7 +5,9 @@ import Base.Primitives structure OpaqueDefs where /- [no_nested_borrows::Pair] -/ - structure pair_t (T1 T2 : Type) where pair_x : T1 pair_y : T2 + structure pair_t (T1 T2 : Type) where + pair_x : T1 + pair_y : T2 /- [no_nested_borrows::List] -/ inductive list_t (T : Type) := @@ -13,16 +15,20 @@ structure OpaqueDefs where | ListNil : list_t T /- [no_nested_borrows::One] -/ - inductive one_t (T1 : Type) := | OneOne : T1 -> one_t T1 + inductive one_t (T1 : Type) := + | OneOne : T1 -> one_t T1 /- [no_nested_borrows::EmptyEnum] -/ - inductive empty_enum_t := | EmptyEnumEmpty : empty_enum_t + inductive empty_enum_t := + | EmptyEnumEmpty : empty_enum_t /- [no_nested_borrows::Enum] -/ - inductive enum_t := | EnumVariant1 : enum_t | EnumVariant2 : enum_t + inductive enum_t := + | EnumVariant1 : enum_t + | EnumVariant2 : enum_t /- [no_nested_borrows::EmptyStruct] -/ - structure empty_struct_t where + structure empty_struct_t where /- [no_nested_borrows::Sum] -/ inductive sum_t (T1 T2 : Type) := @@ -446,10 +452,8 @@ structure OpaqueDefs where /- [no_nested_borrows::StructWithTuple] -/ structure struct_with_tuple_t (T1 T2 : Type) where - struct_with_tuple_p : (T1 × T2) - /- [no_nested_borrows::new_tuple1] -/ def new_tuple1_fwd : Result (struct_with_tuple_t UInt32 UInt32) := Result.ret @@ -476,10 +480,8 @@ structure OpaqueDefs where /- [no_nested_borrows::StructWithPair] -/ structure struct_with_pair_t (T1 T2 : Type) where - struct_with_pair_p : pair_t T1 T2 - /- [no_nested_borrows::new_pair1] -/ def new_pair1_fwd : Result (struct_with_pair_t UInt32 UInt32) := Result.ret diff --git a/tests/lean/misc-no_nested_borrows/lake-manifest.json b/tests/lean/misc-no_nested_borrows/lake-manifest.json new file mode 100644 index 00000000..57b071ca --- /dev/null +++ b/tests/lean/misc-no_nested_borrows/lake-manifest.json @@ -0,0 +1,27 @@ +{"version": 4, + "packagesDir": "./lake-packages", + "packages": + [{"git": + {"url": "https://github.com/leanprover-community/mathlib4.git", + "subDir?": null, + "rev": "4037792ead804d7bfa8868e2c4684d4223c15ece", + "name": "mathlib", + "inputRev?": null}}, + {"git": + {"url": "https://github.com/gebner/quote4", + "subDir?": null, + "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa", + "name": "Qq", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/JLimperg/aesop", + "subDir?": null, + "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690", + "name": "aesop", + "inputRev?": "master"}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee", + "name": "std", + "inputRev?": "main"}}]} diff --git a/tests/lean/misc-no_nested_borrows/lakefile.lean b/tests/lean/misc-no_nested_borrows/lakefile.lean index e4460813..58619110 100644 --- a/tests/lean/misc-no_nested_borrows/lakefile.lean +++ b/tests/lean/misc-no_nested_borrows/lakefile.lean @@ -4,15 +4,9 @@ open Lake DSL require mathlib from git "https://github.com/leanprover-community/mathlib4.git" -package «no_nested_borrows» { - -- add package configuration options here -} +package «no_nested_borrows» {} -lean_lib «Base» { - -- add library configuration options here -} - -lean_lib «NoNestedBorrows» { - -- add library configuration options here -} +lean_lib «Base» {} +@[default_target] +lean_lib «NoNestedBorrows» {} diff --git a/tests/lean/misc-no_nested_borrows/lean-toolchain b/tests/lean/misc-no_nested_borrows/lean-toolchain new file mode 100644 index 00000000..bbf57f10 --- /dev/null +++ b/tests/lean/misc-no_nested_borrows/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2023-01-21 |