Auto implicit argument

Stream: new members

[kana]

How to mark implicit argument as auto, so it will be filled by values with exact type in context automatically?

def printHead [ToString α] (xs : List α) {h : xs ≠ []} := do
  IO.println (xs.head (by assumption))

def f (xs : List Nat) : IO Unit := do
  if h : xs ≠ [] then
    printHead xs

-- don't know how to synthesize implicit argument
--   @printHead Nat instToStringNat xs (_ : xs ≠ [])
-- context:
-- xs: List Nat
-- h: xs ≠ []
-- ⊢ xs ≠ []

[Alex J. Best]

You can do

def printHead [ToString α] (xs : List α) (h : xs ≠ [] := by assumption) := do
  IO.println (xs.head (by assumption))

def f (xs : List Nat) : IO Unit := do
  if h : xs ≠ [] then
    printHead xs

it can't be implicit when you do this for some reason I don't yet understand