e542810e79
This PR adds an example for the Lean hackathon in Paris. It demonstrates how users can implement https://hackmd.io/Qd0nkWdzQImVe7TDGSAGbA
5 lines
79 B
Text
5 lines
79 B
Text
import Lake
|
|
open System Lake DSL
|
|
|
|
package homo
|
|
@[default_target] lean_lib Homo
|