jonaprieto/agda-prop

Issues

• Remove Weaken as a valid constructor

  #21 opened 7 years ago by jonaprieto
  0

• Investigating the performance of thm-find-conjunct vs atp-conjunct from agda-metis

  #16 opened 7 years ago by jonaprieto
  1

• right-associative for conjunction using function from SyntanxExperimantal module

  #17 opened 7 years ago by jonaprieto
  1

• The size of a formula

  #19 opened 7 years ago by jonaprieto
  0

• Comparison between formulas

  #20 opened 7 years ago by jonaprieto
  0

• Use another definition of nnf

  #14 opened 7 years ago by jonaprieto
  1

• Idempotent laws for basic connectives

  #13 opened 7 years ago by jonaprieto
  0

• A useful theorem with normal forms

  #18 opened 7 years ago by jonaprieto
  1

• φ∨⊥-to-φ, and subst⊢∨₁≡ postulated

  #15 opened 7 years ago by jonaprieto
  0

• Contraposition

  #9 opened 7 years ago by jonaprieto
  0

• Links for theorems in the README broken

  #10 opened 7 years ago by jonaprieto
  0

• Theorem required

  #11 opened 7 years ago by jonaprieto
  1

• CNF fails

  #12 opened 7 years ago by jonaprieto
  0

• A new entry about of normal forms in the README

  #5 opened 7 years ago by jonaprieto
  0

• Documenting All Views

  #6 opened 7 years ago by jonaprieto
  0

• Proofs for spliting auxiliar theorems for agda-metis

  #8 opened 7 years ago by jonaprieto
  0

• Provide a proof

  #7 opened 7 years ago by jonaprieto
  0

• README.md plan

  #1 opened 8 years ago by jonaprieto
  0