ExternalFuns.lean « HashmapMain « hashmap_on_disk « lean « tests - aeneas - aeneas rust verifier with a hacky Isabelle backend

summary refs log tree commit diff

path: root/tests/lean/hashmap_on_disk/HashmapMain/ExternalFuns.lean

blob: a5103acc89a6b082a13422bc66edd28a44208353 (plain)

import Base.Primitives
import HashmapMain.Types
import HashmapMain.Opaque

def opaque_defs : OpaqueDefs := by sorry