solar-conflux/lean/learning/lakefile.lean

import Lake
open Lake DSL

package «lean-learning» {
  -- add configuration options here
}
Move stuff around + add lean and idris experiments 2023-10-29 00:02:10 +02:00			`import Lake`
			`open Lake DSL`

Document lean experiments 2023-10-29 00:07:15 +02:00			`package «lean-learning» {`
Move stuff around + add lean and idris experiments 2023-10-29 00:02:10 +02:00			`-- add configuration options here`
			`}`