18 lines
258 B
Lean4
18 lines
258 B
Lean4
import Lake
|
|
open Lake DSL
|
|
|
|
package bidirtt where
|
|
leanOptions := #[
|
|
⟨`pp.unicode.fun, true⟩,
|
|
⟨`autoImplicit, false⟩
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib BidirTT where
|
|
|
|
lean_exe bidirtt where
|
|
root := `Main
|
|
|
|
lean_exe tests where
|
|
root := `Tests
|