jonaprieto/agda-metis

Issues

• Splitting goals: proving atp-split

  #9 opened 7 years ago by jonaprieto
  5

• Theorems to simplify expressions

  #19 opened 7 years ago by jonaprieto
  2

• canonicalize evidence

  #23 opened 7 years ago by jonaprieto
  4

• Normalized Formula data type

  #24 opened 7 years ago by jonaprieto
  1

• atp-conjunct

  #18 opened 7 years ago by jonaprieto
  1

• Missing proofs for auxiliar theorem in Resolve module

  #21 opened 7 years ago by jonaprieto
  1

• Improve the proof for build-∨

  #20 opened 7 years ago by jonaprieto
  1

• Deduce $false in this case

  #5 opened 7 years ago by jonaprieto
  0

• clausify evidence

  #22 opened 7 years ago by jonaprieto
  0

• mix of a reordering ∧ and ∨.

  #17 opened 7 years ago by jonaprieto
  0

• atp-resolve exhibits a pattern

  #13 opened 7 years ago by jonaprieto
  1

• thm-reorder-v omits cases

  #16 opened 7 years ago by jonaprieto
  1

• canonicalize

  #14 opened 7 years ago by jonaprieto
  0

• steps-contraction is correct? I'm not sure at the moment.

  #8 opened 8 years ago by jonaprieto
  3

• Missing case in atp-conjunct, fails projecting.

  #6 opened 8 years ago by jonaprieto
  0