…onym types and UTF8 char literals.

…clarations.

…ppropriate

Fixed support for "this" and constants in reference counting mode.
Removed old obsolete class implementations

Added all tuples till 16 with a script

Support for arrays with 16 dimensions

Feature classes and arrays

Added documentation about target type

Full feat rust

Support for Reference counted pointers everywhere.

Fixed self type for datatypes vs classes
Fixed detection of uninitialized reference counted array

Fixed an issue about elseBranch's statements being in the wrong fork.

No reading of objects, only borrows

Assertion fixed

fixup for feat-rust-classes: Nightly crimes no longer printing anything

…, loops & quantifiers, datatype fields ownership, fixed cloning of closed lambda objects, fixed coercion problems

Fixup for feat-rust-loops

… correctly.

…names escaped

reserved names: {s,S}elf become r#_{s,S}elf rather than r#{s,S}elf + removed them from reserved_rust

Fixup feat-rust-traits expected test
fixup traits - no full qualifier for methods if not necessary

…ctions members in datatypes, reserved names

- PartialEq, Eq, and Default traits not implemented when datatype contains non-equatable types
- note: PartialEq does not have to be manually implemented for parameterized types
- note: Auto-generated implementations of Hash constrain type arguments to be subtypes of DafnyType, not DafnyTypeEq
- Implementations of fmt_print write "<function>" for members of function type
- Implementations of hash ignore members of function type
datatypes: style fixes
reserved names: destructors containing reserved field names avoid field punning

…ironment closures owned

… memory leaks with MIRI

… function outputs

…panic

fixup extern: ExternCompanion

fixup externs: Ensure it works for traits as well. Test for the compilation error

Fixup external classes test

Fixup external classes when no conflict + documentation

Ensure order of imports is deterministic and alphabetic

Fixup advanced externs and patterns

Fixup: no emitting pub use extern if everything is defined. Fixed field change

Fixup externs

Fixup externs: Ensure the default class decl does not need the extern attribute

Fixup externs

fixup externs: Classes are extern means their implementation must be provided externally
Function externs correctly have their full extern path

… in quantifiers

Fixup init value for synonym types

…lambdas

functions: more robust eta-expansion

constants: test to make sure constant lambdas are compiled properly (eta-expanded and type-annotated)

…evel and value-level (variables, etc.) names differently, the latter accounting for reserved fields

…les in scope

- desugaring of elephant operator now declares and initializes head variable after error handling
- as a result, code generation avoids declaring the head variable
- the old type system now avoids duplicating the head variable in scope
- NB: the new type system does not have this fix yet b/c by changing the declaration order of the head variable, a resolver invariant is broken

…e, conversions, etc.

Items and map no longer requires V to have Eq trait

type tests: more general by using is_instance_of_object

…type substitution

…by datatype members

…ersion from Dafny

Fixed regressions

fixup feat-type-synonym-complete

Fixup previous

Map.Keys, .Values and .Items not forcing the clone of the object.
Ensure not possible to create constructorless objects.

… reduce generated code size

…n Rust

# Conflicts:
#	Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs
#	Source/DafnyCore/Backends/Dafny/AST.dfy
#	Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
#	Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
#	Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs
#	Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs
#	Source/DafnyCore/GeneratedFromDafny/DAST.cs
#	Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
#	Source/DafnyCore/GeneratedFromDafny/RAST.cs
#	Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
#	Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs
#	Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/class.dfy.rs.check
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/AutoInit.dfy.rs.check
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/DefaultParameters-Compile.dfy.rs.check
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/arrays.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/borrowing.dfy
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/borrowing.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/bymethod.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/classes.dfy
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/classes.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/loops.dfy
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/loops.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/reserved-names.dfy
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/traits.dfy
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/traits.dfy.expect

…antom variants

Ran "make pr"

…hen necessary

…ames-tests

# Conflicts:
#	Source/DafnyCore/Options/CommonOptionBag.cs

…ithub.com/dafny-lang/dafny into feat-rust-externs-subsets-eta-names-tests

Co-authored-by: Robin Salkeld <[email protected]>