MartyO256/mechanizing-standard-ml

Issues

• Higher-order assumption fails for `tm-of-reg`

  #2 opened 4 years ago by MartyO256
  1

• Invalid hypotheses in `functionality-kd-reg`

  #1 opened 4 years ago by MartyO256
  3

• Ill-typed term errors where the expected type matches the inferred type

  #3 opened 4 years ago by MartyO256
  0

• Totality checking for type constructor inversion lemmas

  #4 opened 4 years ago by MartyO256
  1

• Strenghten term inversion lemmas

  #5 opened 4 years ago by MartyO256
  1