lakefile.lean - BinaryHeap - A toy project about formal validation of a Heap in Lean4

about summary refs log tree commit diff

path: root/lakefile.lean

blob: c1a725e629ab25e8f4695ced6fa582e71dd3b302 (plain) (blame)

import Lake
open Lake DSL

package «BinaryHeap» where

@[default_target]
lean_lib «BinaryHeap» where