You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, we don't have plan to port to Mathlib for some reasons. The main reason is formalizing logic is strongly depending way to formalize or its represent (formulae, deduction system, etc.), so even if we create as "library", we thought it might not be used widely as algebra or else.
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
FormalizedFormalLogic
-
Some people asked about this, we left the answer.
Currently, we don't have plan to port to Mathlib for some reasons. The main reason is formalizing logic is strongly depending way to formalize or its represent (formulae, deduction system, etc.), so even if we create as "library", we thought it might not be used widely as algebra or else.
reference
Beta Was this translation helpful? Give feedback.
All reactions