# Generated by lungo 1.106.540 from Lean 4.34.1 for program tagged_urn_formal. Do not edit.
# A directory of the host package's CMake project (`add_subdirectory`): it builds the program
# and installs it into the module tagged_urn/_formal.

# The runtime this package runs on is the one lungo_py carries.
if(NOT TARGET lungo::runtime_shared)
    find_package(Python COMPONENTS Interpreter REQUIRED)
    execute_process(
      COMMAND "${Python_EXECUTABLE}" -c "import lungo_py; print(lungo_py.cmake_dir())"
      OUTPUT_VARIABLE LUNGO_CMAKE_DIR OUTPUT_STRIP_TRAILING_WHITESPACE COMMAND_ERROR_IS_FATAL ANY)
    find_package(lungo 1.106.540 EXACT CONFIG REQUIRED PATHS "${LUNGO_CMAKE_DIR}" NO_DEFAULT_PATH)
endif()

add_library(tagged_urn_formal_lean SHARED
  program/modules/Init-Core.c
  program/modules/Init-Data-ByteArray-Basic.c
  program/modules/Init-Data-ByteArray-Extra.c
  program/modules/Init-Data-Int-Basic.c
  program/modules/Init-Data-Int-Repr.c
  program/modules/Init-Data-List-Basic.c
  program/modules/Init-Data-Nat-Bitwise-Basic.c
  program/modules/Init-Data-Random.c
  program/modules/Init-Data-Repr.c
  program/modules/Init-Data-String-Basic.c
  program/modules/Init-Data-String-Bootstrap.c
  program/modules/Init-Data-String-Defs.c
  program/modules/Init-Data-String-Iterate.c
  program/modules/Init-Data-String-Modify.c
  program/modules/Init-Data-UInt-Basic.c
  program/modules/Init-Data-UInt-BasicAux.c
  program/modules/Init-Prelude.c
  program/modules/Init-System-IO.c
  program/modules/Init-System-IOError.c
  program/modules/Init-System-ST.c
  program/modules/Init-Util.c
  program/modules/Lean-Data-Iterators-Producers-PersistentHashMap.c
  program/modules/Lean-Elab-Structure.c
  program/modules/TaggedUrn-Constraint.c
  program/modules/TaggedUrn-Exec.c
  program/modules/TaggedUrn-Sorted.c
  program/modules/TaggedUrn-Urn.c
  program/tagged_urn_formal_boundary.c
  program/tagged_urn_formal_program.c
)
target_include_directories(tagged_urn_formal_lean PRIVATE program)
target_compile_features(tagged_urn_formal_lean PRIVATE c_std_11)
# lungo_py looks the program's entry points up by name: a Windows DLL exports its symbols as
# shared libraries elsewhere do.
set_target_properties(tagged_urn_formal_lean PROPERTIES WINDOWS_EXPORT_ALL_SYMBOLS ON)
# The runtime's symbols come from lungo_py's library, loaded first into the process: on
# Windows through its import library, elsewhere resolved when the program is loaded.
if(WIN32)
  target_link_libraries(tagged_urn_formal_lean PRIVATE lungo::runtime_shared)
elseif(APPLE)
  target_link_options(tagged_urn_formal_lean PRIVATE -undefined dynamic_lookup)
endif()
install(TARGETS tagged_urn_formal_lean LIBRARY DESTINATION tagged_urn/_formal RUNTIME DESTINATION tagged_urn/_formal)
