as a lean noob but a datalog novice, could you explain how it ties to lean? I thought of lean as a proof language rather than a programming language. don't you have to write out every step yourself? or.. hrm. is lean actually a pure functional language with dependent types, and the tactics are just functions? or are tactics like type-level functions, but lean can support regular functions too?
as a lean noob but a datalog novice, could you explain how it ties to lean? I thought of lean as a proof language rather than a programming language. don't you have to write out every step yourself? or.. hrm. is lean actually a pure functional language with dependent types, and the tactics are just functions? or are tactics like type-level functions, but lean can support regular functions too?