import Lean.Data.Json

def pi : Lean.JsonNumber := 3.14159

-- It's okay to have concrete-typed definitions, so long as we have a coe to
-- `Any`.