Problem: let has different behaviour from inline signatures

Solution: - We simply demonstrate this clearly a couple of times. Once in commented out code on line 33 in FuncDep.lean and once in this patch, on line 55 in Main.lean.
cognivore · Jul 7, 2022 · 55c9a46 · cognivore · Jul 7, 2022 · 55c9a46
1 parent 64f604e
commit 55c9a46
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/Main.lean b/Main.lean
@@ -47,7 +47,13 @@ def main : IO Unit := do
   IO.println s!"{nₓ}"
   let n₂ : Nat := FuncDep.CountParts_.φ "Tarmogoyf" 'o'
   IO.println s!"{n₂}"
-  let n₃ : Nat := FuncDep.CountParts.φ "Tarmogoyf" 'o'
+  let n₂' := (FuncDep.CountParts_.φ "Tarmogoyf" 'o' : Nat)
+  /-
+  failed to synthesize instance
+    ToString (FuncDep.CountParts_.α String)
+  -/
+  -- IO.println s!"{n₂'}"
+  let n₃ : Nat := FuncDep.CountParts.φ "Magnivore" 'o'
   IO.println s!"{n₃}"
   let n₄ := countNonsense "Paradox Engine"
   IO.println s!"{n₄}"