Bump toolchain to 2022-10-27

[mpenciak]

Changes and notes

lakefile

• defaultTarget -> default_target
• Update dependencies
• Fix a proof that was broken (Lean used to be able to unify [] ≠ [] with cmd ≠ [])
• Using Lean RBTree. Doesn't seem like Lakefiles can use the modules they import????
• TODO (before merge) : Fix CLI import once that PR is merged

Yatima.Datatypes.Lean

• auxDecl is no longer a valid BinderInfo so I eliminated references to it everywhere (in this file, and others)

Yatima.Datatypes.Cid

• Attribute rename: matchPattern -> match_pattern

Yatima.Datatypes.Store

• RBTree -> RBSet rename
• RBMap.fold -> RBMap.foldl rename

Yatima.Ipld.To/FromIpld

• Remove auxDecl references
• RBTree -> RBSet

Yatima.Ipld.PrimCids

• RBMap now needs explicit comparison

Yatima.Compiler.Compiler

• RBMap now needs explicit comparison

Yatima.Compiler.Printing

• Remove auxDecl references

Yatima.Compiler.Utils

• The Lean data structure Lean.SMap is built out of Lean.Hashmap, so no migratin of the Hashmaps to the Std namespace
• Std does not havePersistentHashMap, so change Std to Lean namespaces for those as well

Yatima.Transpiler.Simp/Yatima.Transpiler.LurkFunctions/TranspileM/

• Fix Lurk.DSL -> Lurk.Syntax.DSL import and fix the namespaces. This is common throughout the Transpiler fixes, so I'll group them here.

Yatima.Transpiler.Utils

• Above fixes
• Added a couple functions that were used before we had mut rec but were taken out of the Lurk.lean repo. This is only a temporary fix for now because I imagine the refactor will mean we won't actually need them. In particular added back mkMutualBlock and toImplicitLambda back

Yatima.Transpiler.Transpiler

• Above fixes
• change in .app₀/.app -> .app were fixed (adding in extra logic around Option args)
• Add in the extra comm, commit, and hide constructors with no logic behind them

Yatima.Cli

• RBMap.fold -> RBMap.foldl
• Lurk.Eval -> Lurk.Evaluation.Eval

TestUtils

• Deleted ExprGenerator (it's unusued, broken, badly coded, and doesn't seem very helpful)
• Lurk.Eval -> Lurk.Evaluation.Eval

Fixtures

• implementedBy -> implemented_by
• RBMap now needs the comparison explicitly
• Expr -> TC.Expr name change
• Not fixed: prelude.lean is the old prelude. Do we want to use the new one? (obviously the prelude typechecking test is failing because of this)

Tests

• Lurk DSL namespace changes
• Thunks don't seem to have a coercion from α to Thunk α anymore? (using Thunk.pure now)