Lean: translate some first type rather trivial type signatures

[javra]

Translates

function foo(x : unit) -> unit = {
  return x
}

to

def foo (x : Unit) : Unit :=
  _

[github-actions[bot]]

Test Results

   10 files  ±0     22 suites  ±0   0s ⏱️ ±0s   701 tests ±0    701 ✅ ±0  0 💤 ±0  0 ❌ ±0  2 181 runs  ±0  2 180 ✅ ±0  1 💤 ±0  0 ❌ ±0 

Results for commit ce339cfc. ± Comparison against base commit f89c7d76.

:recycle: This comment has been updated with latest results.

[bacam]

The changes to sail_plugin_lean.ml were removed in the merge, did you mean to keep them? Also, is it worth having that trivial example in the repository?

[javra]

@bacam Thanks, that wasn't intended

[javra]

Yes, the trivial example should maybe instead be a test. I haven't looked at how the tests are done so far, will hopefully find the time to do that next week.