ExternalFuns.lean « External « misc-external « lean « tests - aeneas - aeneas rust verifier with a hacky Isabelle backend

summary refs log tree commit diff

path: root/tests/lean/misc-external/External/ExternalFuns.lean

blob: 6bd4f4a938f80e12da7595ff6b16d1ccebe69609 (plain)

import Base.Primitives
import External.Types
import External.Opaque

def opaque_defs : OpaqueDefs := sorry