Code

FFI with cvc5#70

Code

Closed

tomaz1502 wants to merge 15 commits intomainufmg-smite/lean-smt:mainfrom cvc5Proofsufmg-smite/lean-smt:cvc5ProofsCopy head branch name to clipboard

+175

Commits

Commits on Oct 12, 2023

• first tentative to represent cvc5 proofs

  tomaz1502

  committed
  f4c9a0e

  Copy full SHA for f4c9a0e

• fix on parsing string tactics and shorter types

  tomaz1502

  committed
  8ba2006

  Copy full SHA for 8ba2006

Commits on Oct 18, 2023

• infrastructure for running cvc5 proofs

  tomaz1502

  committed
  61c5ff3

  Copy full SHA for 61c5ff3

• removing unused constant

  tomaz1502

  committed
  1ea681e

  Copy full SHA for 1ea681e

• simplifying

  tomaz1502

  committed
  34c5b56

  Copy full SHA for 34c5b56

• changing Tac to abbrev String

  tomaz1502

  committed
  bd645c0

  Copy full SHA for bd645c0

• removing type in scope and Cvc5Proof

  tomaz1502

  committed
  09f1023

  Copy full SHA for 09f1023

• fixing test

  tomaz1502

  committed
  0e7fbd9

  Copy full SHA for 0e7fbd9

Commits on Oct 19, 2023

• new pf constructor: hyp

  tomaz1502

  committed
  d4b3097

  Copy full SHA for d4b3097

• added proof for modus ponens

  tomaz1502

  committed
  2248476

  Copy full SHA for 2248476

Commits on Oct 24, 2023

• (hackish) implementation for scope

  tomaz1502

  committed
  690be60

  Copy full SHA for 690be60

• clean up

  tomaz1502

  committed
  34385c4

  Copy full SHA for 34385c4

• clarifying comment

  tomaz1502

  committed
  69469e0

  Copy full SHA for 69469e0

Commits on Oct 25, 2023

• fix hidden bug

  tomaz1502

  committed
  d089718

  Copy full SHA for d089718

Commits on Nov 8, 2023

• removing unnecessary do

  tomaz1502

  committed
  9fe2b63

  Copy full SHA for 9fe2b63