HOL-Theorem-Prover/HOL

Issues

• Defining multiple independent functions in the same definition block.

  #1324 opened a month ago by Eric-C-Hall
  4

• Q.MATCH_ABBREV_TAC only uses one parse of its pattern, not all possible parses

  #1325 opened a month ago by Eric-C-Hall
  0

• Make "modern" Definition syntax extensible

  #1316 opened 2 months ago by dnezam
  0

• Quote syntax parses incorrectly

  #1313 opened 2 months ago by dnezam
  1

• Ignore assumption directive for simplifier

  #1220 opened 2 months ago by mn200
  0

• EVAL monitoring should be able to stop the computation

  #1262 opened 2 months ago by mn200
  5

• `Thm.SPEC` appears to hang in certain degenerate conditions

  #1300 opened 2 months ago by someplaceguy
  0

• Awful error in inductive relations arising from inconsistent handling of schem vars

  #1296 opened 3 months ago by talsewell
  2

• New Quote syntax isn't highlighted correctly in emacs

  #1290 opened 3 months ago by myreen
  1

• reorder and rename quantifiers by specifying pattern(s) underneath

  #1259 opened 5 months ago by mn200
  1

• Feature requests to the generic graph theory

  #1278 opened 3 months ago by binghe
  2

• Optional heaps in Holmake

  #1283 opened 3 months ago by talsewell
  8

• `EVAL "NUM_CEILING 0"` doesn't work

  #1281 opened 4 months ago by someplaceguy
  0

• `RealField.REAL_ARITH_TAC` unable to prove `-1r / x - 1 / -x >= 0`

  #1280 opened 4 months ago by someplaceguy
  5

• General modern "quotation" syntax support

  #1229 opened 4 months ago by mn200
  0

• Special syntax for nested/sequence of sum_CASE constants

  #1276 opened 4 months ago by mn200
  0

• case_pred_disj_of ``:'a # 'b`` fails

  #1260 opened 4 months ago by mn200
  0

• Error trying to build on MacOs

  #1270 opened 4 months ago by Oliver-Bagin
  1

• Unexpected error with `DefnBase.one_line_ify`

  #1250 opened 5 months ago by hrutvik
  0

• add patCases_on tactic

  #1258 opened 5 months ago by mn200
  0

• C++ compilation failure of `src/HolSat/sat_solvers/zc2hs` on macOS

  #1233 opened 5 months ago by binghe
  4

• Fix intLib to avoid noisy output

  #1241 opened 6 months ago by acjf3
  1

• Moscow ML builds broken after `cv_translator`

  #1226 opened 7 months ago by binghe
  1

• A broken generated HTML theory in non-Unicode mode

  #1225 opened 7 months ago by binghe
  2

• Q.PAT_X_ASSUM returns bad errors

  #1230 opened 7 months ago by mn200
  0

• Add a q.subpat_{x_,}assum

  #1222 opened 7 months ago by mn200
  0

• Add spec form to cover both `INST` and `SPEC` of theorems

  #1221 opened 7 months ago by mn200
  0

• intLib.{ARITH,COOPER}_PROVE can't prove certain goals

  #1207 opened 8 months ago by someplaceguy
  5

• "intLib.ARITH_PROVE ``0n = x * Num 0i``" fails unexpectedly

  #1203 opened 8 months ago by someplaceguy
  1

• intLib.ARITH_PROVE raises exception `NotFound`

  #1209 opened 8 months ago by someplaceguy
  1

• Building HOL4 will crash with latest Apple update of Xcode

  #1147 opened 10 months ago by jhlchan
  3

• SAT_ORACLE gives wrong answers

  #1170 opened a year ago by myreen
  11

• Limits on the number of jobs for Holmake?

  #1163 opened a year ago by barakeel
  2

• Allow "reduced" info printing in emacs

  #1153 opened a year ago by mn200
  1

• Use rule-names instead of conjunctions in Inductive definitions

  #1154 opened a year ago by mn200
  1

• `Holmake: Exception: Subscript` when building HOL with -j12 or greater (but not -j11 or lower)

  #1158 opened a year ago by someplaceguy
  5

• Alpha turns into a by accident

  #1140 opened a year ago by myreen
  0

• Remove/Name Anonymous Rewrite for NUM_CEILING

  #1149 opened a year ago by jdyeager
  1

• Tools should report config files' location

  #1141 opened a year ago by mn200
  0

• Some small typos in the doc

  #1133 opened a year ago by fblanqui
  2

• Proof failed but Holmake doesn't report it

  #1110 opened a year ago by binghe
  6

• Command sequence for installing HOL's OpenTheory packages

  #1121 opened a year ago by binghe
  3

• Use kernel compute feature in HOL4 simplifier, decision procedures, and EVAL

  #1118 opened a year ago by myreen
  6

• Manual Makefile

  #1108 opened 2 years ago by fblanqui
  5

• Emacs mode doesn't have M-h H in menu

  #1098 opened 2 years ago by mn200
  0

• emacs mode: package the lisp code for it to be released in a package archive

  #1103 opened 2 years ago by chenzhawyang
  1

• emacs mode should choose HOL executable based on lastmaker file (if any)

  #1101 opened 2 years ago by mn200
  1

• Configure failure on macOS: Failed to make mlyacc (Fail "Command failed")

  #1092 opened 2 years ago by barracuda156
  4

• Failure to build on Android/termux

  #1099 opened 2 years ago by SylNah
  6

• Store location information about where theorems were proved in Theory.sig files

  #1094 opened 2 years ago by mn200
  0