Lean: List Int to Nat conversion

[Alasdair]

One test fails with (The aptly named list_torture):

error: ././././Out.lean:126:41: application type mismatch
  Exc_list_int xs
argument
  xs
has type
  List Nat : Type
but is expected to have type
  List Int : Type

so we need at least a List Nat to List Int conversion. But there is likely a more general problem when we start nesting types like list(option(list(nat))) and list(option(list(int))) in Sail.

[Alasdair]

I made a test case of the awkward version:

has type
  List (Option (wrapper (List (Option (wrapper (List (Option (wrapper Nat)))))))) : Type
but is expected to have type
  List (Option (wrapper (List (Option (wrapper (List (Option (wrapper Int)))))))) : Type

[javra]

I think there's not going to be a problem with the nested cases because of the way we'd set up the coercions.