Skip to content

Commit

Permalink
Add require "foundry.md" to kontrol init generated lemmas file (#757
Browse files Browse the repository at this point in the history
)

Co-authored-by: rv-jenkins <admin@runtimeverification.com>
Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>
  • Loading branch information
3 people authored Aug 9, 2024
1 parent 8c58702 commit b78077e
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/kontrol/utils.py
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,9 @@ def append_to_file(file_path: Path, content: str) -> None:


def empty_lemmas_file_contents() -> str:
return """module KONTROL-LEMMAS
return """require "foundry.md"
module KONTROL-LEMMAS
// Your lemmas go here
// Not sure what to do next? Try checking the documentation for writing lemmas: https://docs.runtimeverification.com/kontrol/guides/advancing-proofs/kevm-lemmas
Expand Down

0 comments on commit b78077e

Please sign in to comment.