.python-version
FormalSW.lean
MANIFEST.in
README.adoc
build_support.py
formalsw
lakefile.toml
lean-toolchain
pyproject.toml
test
formalsw.egg-info/PKG-INFO
formalsw.egg-info/SOURCES.txt
formalsw.egg-info/dependency_links.txt
formalsw.egg-info/entry_points.txt
formalsw.egg-info/top_level.txt
lang/runtime.py
lang/spec_setup.py
lang/py/call_support.py
lang/py/contracts.py
lang/py/data_ast.py
lang/py/defaults.py
lang/py/global_inputs.py
lang/py/graph_equivalence.py
lang/py/imports.py
lang/py/lean_frontend.py
lang/py/linking.py
lang/py/mutable_support.py
lang/py/object_snapshot.py
lang/py/quotation.py
lang/py/spec_frontend.lean
lang/py/support.py
lang/py/trial.py
lang/py/FormalSW/Calls.lean
lang/py/FormalSW/DataRuntime.lean
lang/py/FormalSW/Execution.lean
lang/py/FormalSW/Globals.lean
lang/py/FormalSW/GraphEquivalence.lean
lang/py/FormalSW/HeapCalls.lean
lang/py/FormalSW/Linking.lean
lang/py/FormalSW/Math.lean
lang/py/FormalSW/Model.lean
lang/py/FormalSW/MutableGlobals.lean
lang/py/FormalSW/Parallel.lean
lang/py/FormalSW/ParallelLiveness.lean
lang/py/FormalSW/PyValue.lean
lang/py/FormalSW/Python.lean
lang/py/FormalSW/Quotation.lean
lang/py/FormalSW/Runtime.lean
lang/py/FormalSW/Sorting.lean
lang/py/FormalSW/Strings.lean
lang/py/FormalSW/Syntax.lean
lang/py/builtin/function.lean
lang/py/builtin/function.py
lang/py/builtin/function.py.lean
lang/py/builtin/type/bool.lean
lang/py/builtin/type/bool.py
lang/py/builtin/type/bool.py.lean
lang/py/builtin/type/bytearray.lean
lang/py/builtin/type/bytearray.py
lang/py/builtin/type/bytearray.py.lean
lang/py/builtin/type/bytes.lean
lang/py/builtin/type/bytes.py
lang/py/builtin/type/bytes.py.lean
lang/py/builtin/type/comparison.lean
lang/py/builtin/type/contextmanager.lean
lang/py/builtin/type/contextmanager.py
lang/py/builtin/type/contextmanager.py.lean
lang/py/builtin/type/core.lean
lang/py/builtin/type/descriptor.lean
lang/py/builtin/type/descriptor.py
lang/py/builtin/type/descriptor.py.lean
lang/py/builtin/type/dict.lean
lang/py/builtin/type/dict.py
lang/py/builtin/type/dict.py.lean
lang/py/builtin/type/dictview.lean
lang/py/builtin/type/dictview.py
lang/py/builtin/type/dictview.py.lean
lang/py/builtin/type/int.lean
lang/py/builtin/type/iterator.lean
lang/py/builtin/type/iterator.py
lang/py/builtin/type/iterator.py.lean
lang/py/builtin/type/list.lean
lang/py/builtin/type/memoryview.lean
lang/py/builtin/type/object.lean
lang/py/builtin/type/range.lean
lang/py/builtin/type/range.py
lang/py/builtin/type/range.py.lean
lang/py/builtin/type/sequence.lean
lang/py/builtin/type/set.lean
lang/py/builtin/type/set.py
lang/py/builtin/type/set.py.lean
lang/py/builtin/type/slice.lean
lang/py/builtin/type/slice.py
lang/py/builtin/type/slice.py.lean
lang/py/builtin/type/special.lean
lang/py/builtin/type/str.lean
lang/py/builtin/type/str.py
lang/py/builtin/type/str.py.lean
lang/py/builtin/type/subsequence.lean
lang/py/builtin/type/super.lean
lang/py/builtin/type/truth.lean
lang/py/builtin/type/tuple.lean
lang/py/builtin/type/tuple.py
lang/py/builtin/type/tuple.py.lean
lang/py/builtin/type/type.lean
src/formalsw/__init__.py
src/formalsw/__main__.py
src/formalsw/cli.py
tests/package_checks
tests/py/bit_length_checks
tests/py/builtin_coverage
tests/py/builtin_models.lean
tests/py/builtin_python_models.py
tests/py/bytes_checks
tests/py/bytes_literals.py
tests/py/bytes_literals.py.lean
tests/py/call_checks
tests/py/contract_checks
tests/py/default_checks
tests/py/defaults.py
tests/py/defaults.py.lean
tests/py/division.py
tests/py/division.py.lean
tests/py/equiv_throw.py
tests/py/equiv_throw.py.lean
tests/py/generator_sums.py
tests/py/generator_sums.py.lean
tests/py/globals.py
tests/py/globals.py.lean
tests/py/graph_equivalence_checks
tests/py/heap_call_checks
tests/py/heap_calls.py
tests/py/heap_calls.py.lean
tests/py/heap_ranges.py
tests/py/heap_ranges.py.lean
tests/py/int_bit_length.py
tests/py/int_bit_length.py.lean
tests/py/link_checks
tests/py/link_reference.py
tests/py/link_reference.py.lean
tests/py/linked_calls.py
tests/py/linked_calls.py.lean
tests/py/loop_control.py
tests/py/loop_control.py.lean
tests/py/math_gcd.py
tests/py/math_gcd.py.lean
tests/py/math_gcd_checks
tests/py/math_isqrt.py
tests/py/math_isqrt.py.lean
tests/py/math_module_checks
tests/py/math_modules.py
tests/py/math_modules.py.lean
tests/py/maximum.py
tests/py/maximum.py.lean
tests/py/mutable_global_checks
tests/py/mutable_globals.py
tests/py/mutable_globals.py.lean
tests/py/object_equivalence.lean
tests/py/object_equivalence.py
tests/py/parallel_calls.py
tests/py/parallel_calls.py.lean
tests/py/parallel_checks
tests/py/parallel_liveness.lean
tests/py/parallel_liveness.py
tests/py/parallel_liveness.py.lean
tests/py/parallel_semantics.lean
tests/py/parallel_shared_counter.py
tests/py/parallel_shared_counter.py.lean
tests/py/power_checks
tests/py/powers.py
tests/py/powers.py.lean
tests/py/project_checks
tests/py/quotation_checks
tests/py/range_sum.py
tests/py/range_sum.py.lean
tests/py/range_sum_checks
tests/py/raw_lean.py
tests/py/raw_lean.py.lean
tests/py/recursive_calls.py
tests/py/recursive_calls.py.lean
tests/py/requires.py
tests/py/requires.py.lean
tests/py/requires_module.py
tests/py/requires_module.py.lean
tests/py/setup_checks
tests/py/sort.py
tests/py/sort.py.lean
tests/py/stepped_ranges.py
tests/py/stepped_ranges.py.lean
tests/py/string_checks
tests/py/strings.py
tests/py/strings.py.lean
tests/py/support_checks
tests/py/termination.py
tests/py/termination.py.lean
tests/py/test_support.py
tests/py/throws.py
tests/py/throws.py.lean
tests/py/throws_syntax.lean
tests/py/tuple_assignments.py
tests/py/tuple_assignments.py.lean
tests/py/typing.py
tests/py/typing.py.lean
tests/py/fail/global_legacy.py
tests/py/fail/global_mutable.py
tests/py/fail/missing_lean.py
tests/py/fail/missing_required.py
tests/py/fail/missing_required.py.lean
tests/py/fail/parallel_missing_lock.py
tests/py/fail/parallel_missing_lock.py.lean
tests/py/fail/sorry.py
tests/py/fail/sorry.py.lean
tests/py/fail/this_function_annotation.py
tests/py/fail/this_function_arity.py
tests/py/fail/dir/fail.py
tests/py/fail/dir/fail.py.lean
tests/py/fail/dir/pass.py
tests/py/fail/dir/pass.py.lean
tests/py/fail/unsupported/a_blocked.py
tests/py/fail/unsupported/b_mixed.py
tests/py/fail/unsupported/b_mixed.py.lean
tests/py/fail/unsupported/c_supported.py
tests/py/fail/unsupported/c_supported.py.lean
tests/py/fail/unsupported/precondition.py