Process complex LHS patterns in function rules (#4757)

Eliminates patterns that are not supported by Lean from the LHS of
function rules.

For example, since `_List_` is a function, instead of matching the last
item of a list as

```lean
noncomputable def _2ede380 : SortList → Option SortInt
  | _List_ _Gen0 (ListItem (SortKItem.inj_SortInt I)) => ...
  | _ => none
```

the following definition is generated:

```lean
noncomputable def _2ede380 : SortList → Option SortInt
  | _Pat0 => match (ListHook SortKItem).split _Pat0.coll 0 1 with
    | some ([], _Gen0, [SortKItem.inj_SortInt I]) => ...
    | _ => none
```

where `split` is repsonsible for deconstructing the list into prefix,
middle and suffix.

Author: tothtamas28

pyk/poetry.lock

@@ -23,6 +23,7 @@ cookiecutter = "^2.6.0"
 filelock = "^3.9.0"
 graphviz = "^0.20.1"
 hypothesis = "^6.103.1"
+networkx = "^3.4.2"
 psutil = "^5.9.5"
 pybind11 = "^2.10.3"
 pytest = "*"
@@ -97,3 +98,7 @@ ignore_missing_imports = true
 [[tool.mypy.overrides]]
 module = "cookiecutter.*"
 ignore_missing_imports = true
+
+[[tool.mypy.overrides]]
+module = "networkx"
+ignore_missing_imports = true