9 lines
132 B
Plaintext
9 lines
132 B
Plaintext
|
import Lake
|
||
|
|
open System Lake DSL
|
||
|
|
|
||
|
|
package callee
|
||
|
|
|
||
|
|
@[default_target]
|
||
|
|
lean_lib Callee where
|
||
|
|
defaultFacets := #[LeanLib.sharedFacet]
|