expln/metamath-lamp

Issues

• Variables cannot unify with themselves

  #198 opened 9 months ago by CatsAreFluffy
  2

• [question]: How to add an axiom?

  #200 opened 3 months ago by volisoft
  0

• Error when '.,' appears in disjoints

  #199 opened 5 months ago by BTernaryTau
  1

• Improvements for the Merge dialog

  #188 opened a year ago by expln
  1

• Set the default value of "Allow new variables" in the bottom-up prover to false

  #180 opened a year ago by expln
  0

• An assertion tab crashes if the assertion proof contains errors

  #184 opened a year ago by expln
  0

• Search is too slow

  #186 opened a year ago by expln
  0

• Use the same width for all labels on the Editor tab

  #179 opened a year ago by expln
  0

• Add search by description

  #178 opened a year ago by expln
  0

• Unify hangs for certain statements/theorems

  #175 opened a year ago by BTernaryTau
  2

• Error when < appears in description

  #174 opened a year ago by BTernaryTau
  1

• Reorder variables in DV conditions

  #172 opened a year ago by BTernaryTau
  3

• Unify prefers mathbox theorems over identical core set.mm theorems (e.g. frege27 and id)

  #163 opened a year ago by BTernaryTau
  5

• Unable to manually add disjoints on mobile

  #164 opened a year ago by BTernaryTau
  2

• Bottom-up prover adds unnecessary disjoints

  #166 opened a year ago by BTernaryTau
  8

• Make it possible to see more available proofs in the bottom-up prover

  #169 opened a year ago by expln
  0

• Idea: New fragment selector button "insert or elide"

  #121 opened a year ago by david-a-wheeler
  25

• Keep working on disconnect from network

  #161 opened a year ago by david-a-wheeler
  1

• When substituting, always use the most recent selections

  #155 opened a year ago by CatsAreFluffy
  1

• Duplicate up button

  #154 opened a year ago by CatsAreFluffy
  3

• In explorer allow selection of final type (low priority)

  #111 opened a year ago by david-a-wheeler
  0

• Add transitively skipped assertions option

  #152 opened a year ago by CatsAreFluffy
  2

• By default don't use discouraged syntax nor later syntax

  #108 opened a year ago by david-a-wheeler
  4

• Allow merging multiple statements with one merge button click

  #149 opened a year ago by CatsAreFluffy
  5

• Multiple editor tabs

  #153 opened a year ago by CatsAreFluffy
  1

• Notes make the results non-JSON

  #140 opened a year ago by david-a-wheeler
  2

• Can't apply a substitution when there are invalid substitutions

  #151 opened a year ago by CatsAreFluffy
  1

• Warn the user when a substitution is going to change a hypotheses or the goal statement

  #146 opened a year ago by expln
  0

• Allow shrinking to a single symbol in fragment selector (low priority)

  #112 opened a year ago by david-a-wheeler
  3

• Additions for later versions - discussion

  #118 opened 2 years ago by david-a-wheeler
  7

• Question on unused functions

  #135 opened a year ago by billh0420
  2

• In visualizations, don't repeat if conclusion is all constants (low priority)

  #115 opened a year ago by david-a-wheeler
  2

• Add delete (trash can) when editing Description, Variables, and Disjoints (low priority)

  #123 opened a year ago by david-a-wheeler
  2

• Alt+click doesn't edit label and step type when "long click" is enabled

  #138 opened a year ago by expln
  0

• Prohibit substitutions which modify global essential statements

  #144 opened a year ago by expln
  0

• Question on suppressed warning 23

  #142 opened a year ago by billh0420
  1

• Question on suppressed warning 45

  #141 opened a year ago by billh0420
  3

• Question on createDomProps in the file Xml_to_React.res

  #137 opened a year ago by billh0420
  1

• Overflow editor icon bar icons into hamburger

  #134 opened a year ago by david-a-wheeler
  0

• Unclear why bottom-up prover is missing a possible proof (the one I've been using)

  #127 opened 2 years ago by david-a-wheeler
  17

• Visualization bug: On visualization, resulting statement is dragged down to next line

  #116 opened 2 years ago by david-a-wheeler
  1

• Embed the "current version of Metamath-lamp" in the exported JSON

  #128 opened 2 years ago by expln
  0

• Fix compilation warning 44

  #125 opened 2 years ago by billh0420
  2

• More fix compilation warnings

  #122 opened 2 years ago by billh0420
  3

• Announce the release of v11?

  #120 opened 2 years ago by david-a-wheeler
  5

• Implement "Shortened header" view option

  #119 opened 2 years ago by expln
  0

• Be able to load URL in non-TEMP mode

  #114 opened 2 years ago by david-a-wheeler
  1

• Enable display of variable types (low priority)

  #110 opened 2 years ago by david-a-wheeler
  0

• Make TEMP mode (temporary mode) more obvious

  #117 opened 2 years ago by david-a-wheeler
  3

• Generate shorter URLs (low priority)

  #109 opened 2 years ago by david-a-wheeler
  3