Code

Simple coq lemmas#36

Code

Merged

septract merged 30 commits intomainrems-project/cn-tutorial:mainfrom simpl-coq-lemmasrems-project/cn-tutorial:simpl-coq-lemmasCopy head branch name to clipboardJul 11, 2024

+571-31

Commits

Commits on May 28, 2024

• Add README with how to build coq lemmas

  scuellar

  committed
  71e2150

  Copy full SHA for 71e2150

• Add examples

  scuellar

  committed
  f67c2c0

  Copy full SHA for f67c2c0

• Add build files

  scuellar

  committed
  269f916

  Copy full SHA for 269f916

Commits on Jun 10, 2024

• Add and reorder examples

  scuellar

  committed
  c1f94ef

  Copy full SHA for c1f94ef

• Add examples and ignore automatically generated files

  scuellar

  committed
  9d10f7e

  Copy full SHA for 9d10f7e

• Ignore more automatic coq files

  scuellar

  committed
  e7268c4

  Copy full SHA for e7268c4

Commits on Jun 19, 2024

• adding examples

  scuellar

  committed
  425b068

  Copy full SHA for 425b068

• Merge branch 'main' into simpl-coq-lemmas

  scuellar

  committed
  1bc88fe

  Copy full SHA for 1bc88fe

Commits on Jun 24, 2024

• Clarity

  scuellar

  committed
  15544d9

  Copy full SHA for 15544d9

Commits on Jul 9, 2024

• Typos

  scuellar

  committed
  24e43ce

  Copy full SHA for 24e43ce

• Clarify examples

  scuellar

  committed
  8b18f3d

  Copy full SHA for 8b18f3d

Commits on Jul 10, 2024

• Add new script for checking coq extraction

  scuellar

  committed
  e42511c

  Copy full SHA for e42511c

• add the script for checking coq extraction

  scuellar

  committed
  4cee296

  Copy full SHA for 4cee296

• Explain the new organization, including Coq lemmas.

  scuellar

  committed
  b0b7ead

  Copy full SHA for b0b7ead

• Generalize process_files and use it to check Coq extraction

  scuellar

  committed
  6fce7fa

  Copy full SHA for 6fce7fa

• Ignore the build files

  scuellar

  committed
  3fcc4c7

  Copy full SHA for 3fcc4c7

• Ignore coq files, except the proofs. This affects only the example-archive

  scuellar

  committed
  14988a6

  Copy full SHA for 14988a6

• Add the proofs

  scuellar

  committed
  cb04df9

  Copy full SHA for cb04df9

• Move examples that fail to build/incomplete proofs.

  scuellar

  committed
  cbabefd

  Copy full SHA for cbabefd

• Fix the popd bug and add titles to the two sections.

  scuellar

  committed
  156c4f0

  Copy full SHA for 156c4f0

• Move the build folder prototype to the parent directory to be used by any other examples set.

  scuellar

  committed
  b1f959a

  Copy full SHA for b1f959a

• Foolproof build

  scuellar

  committed
  03339e5

  Copy full SHA for 03339e5

• README details

  scuellar

  committed
  fe58f29

  Copy full SHA for fe58f29

• remove old build folder

  scuellar

  committed
  69a793e

  Copy full SHA for 69a793e

• clean up

  scuellar

  committed
  f39bb7f

  Copy full SHA for f39bb7f

Commits on Jul 11, 2024

• Fix Typos

  scuellar

  committed
  8570aff

  Copy full SHA for 8570aff

• Add clarity

  scuellar

  committed
  5f704cc

  Copy full SHA for 5f704cc

• Tidy up typos and some script things

  septract

  committed
  4d5f28b

  Copy full SHA for 4d5f28b

• Readme tweaks

  septract

  committed
  4ec3023

  Copy full SHA for 4ec3023

• Deactivate CI for Coq to make the merge easier

  septract

  committed
  553f94f

  Copy full SHA for 553f94f