First login?
Lost password?
 
 
 
mailing-list for TeXmacs Users

Text archives Help


[TeXmacs] Idea: Convert axioms into theorem conditions


Chronological Thread 
  • From: Victor Porton <address@hidden>
  • To: TeXmacs <address@hidden>
  • Subject: [TeXmacs] Idea: Convert axioms into theorem conditions
  • Date: Sun, 16 Feb 2014 22:16:29 +0200
  • Envelope-from: address@hidden
I suggest to add the following feature to Coq:

Make a modified "Import" statement (possible syntax: "Import Safe
MODULENAME.").

This would transform every axiom (or parameter) in the imported module into a
theorem condition, just like as it is done with sections.

This is especially useful for researching interrelations of several different
axiom systems.

--
Victor Porton - http://portonvictor.org

  • [TeXmacs] Idea: Convert axioms into theorem conditions, Victor Porton, 02/16/2014

Archive powered by MHonArc 2.6.19.

Top of page