Open Seasawher opened 2 weeks ago
import Lean open Lean #eval show CoreM Unit from do let env ← getEnv println! env.constants.toList.length
特に応用例は今のところ思いつかない