| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2025-08-23 | Update Token.hsHEADmain | adelon | |
| 2025-08-14 | Improve scanning | adelon | |
| Fixes scanning of relation symbols and adds a few error cases for function symbols. | |||
| 2025-08-12 | Relax function symbol definitions | adelon | |
| Extra assumptions are simply discarded for now. | |||
| 2025-08-12 | Allow relation symbols with parameters | adelon | |
| Parameters must follow the relation symbol and be surrounded by braces, like so: `\rel{x}{y}{z}`. This attempt is still brittle/broken in a few ways: - It makes using braces in creative ways in mixfix notation ambiguous. - It does not verify that the parameters are used in a consistent manner for each symbol. It essentially allows users to define `a\MyRel b` and `a\MyRel{x} b` (and ones with even more parameters). - It allows parameters for all relation symbols, even for those where it makes no sense in ordinary TeX markup, e.g. `a <{x} b`. | |||
| 2025-07-31 | Remove unused keyword | adelon | |
| 2025-07-16 | Relax label syntax | adelon | |
| 2025-07-16 | Add quantified calcs and relax tokenization | adelon | |
| Use an `\iff`-calc to speed up `union_as_unions`. Also remove `in_implies_neq` which seems to interact badly with the choice axiom used by superposition-based proofs like Vampire in cut-down problems. | |||
| 2025-07-04 | Update Adapt.hs | adelon | |
| 2025-07-04 | Update Adapt.hs | adelon | |
| 2025-07-04 | Forward compat | adelon | |
| 2025-07-04 | Fix whitespace | adelon | |
| 2025-07-02 | Create SmtLib.hs | adelon | |
| 2025-07-02 | Add TODO | adelon | |
| 2025-07-02 | Merge pull request #2 from Simon-Kor/main | adelon | |
| Merge (finally) | |||
| 2024-09-18 | working commit | Simon-Kor | |
| 2024-09-17 | Corrected Math Env Parsing | Simon-Kor | |
| Since Latex has a really specify syntax for \begin{cases} ... \end{cases} The math mode in tokenizing had to be setup correctly. | |||
| 2024-09-03 | Hot fix | Simon-Kor | |
| Hot Fix for the wrong Asumtion creation. Now the function will have a image. | |||
| 2024-08-27 | Feature Complete | Simon-Kor | |
| Finalised the proof output and goals. The Local Function definition now producces a Function f with the right domain and range, together with the rules presented in cases. Then proof goal of this local definition is set to for all x we have x is element of dom(f) if and only if x is in exactly one of the subdomains. This suffices as welldefindness check on f, besides the right range. Further checks that should be implemented are the correct range of the function. And optional subproof such that the presented goal can be check easily. | |||
| 2024-08-27 | ambigus parse fix. The proof goal must be changed, | Simon-Kor | |
| since now some could define a function with overlapping and worng subdomains | |||
| 2024-08-27 | Experimental working commit, programm will compile | Simon-Kor | |
| But the Proof that the domain of the local function is not right. Also if in the definition of our local function we just use f(x) = x then we get a technical ambigus parse | |||
| 2024-08-26 | Implemented the checking for local functions. | Simon-Kor | |
| 2024-08-26 | Non finished attemped to translate a local | Simon-Kor | |
| function defintion from abstract to internal | |||
| 2024-08-26 | I implemented a parsing rule in concrete.hs | Simon-Kor | |
| for local functions and a abstract type in abstract.hs for the proof data structure. | |||
| 2024-08-24 | First atemped to write a new way of local function defintion | Simon-Kor | |
| 2024-08-24 | hlint suggestion | Simon-Kor | |
| 2024-08-24 | Added/Fixed comments | Simon-Kor | |
| 2024-08-12 | way way more urysohn | Simon-Kor | |
| 2024-08-12 | more more way more urysohn | Simon-Kor | |
| 2024-08-07 | Created first urysohn formalization | Simon-Kor | |
| 2024-07-23 | Formatting | adelon | |
| 2024-07-23 | Update prover answer prefixes | adelon | |
| 2024-07-06 | Formalisation of rationals. | Simon-Kor | |
| 2024-07-06 | Formalisation of integers. | Simon-Kor | |
| 2024-06-25 | Add `\neg` | adelon | |
| 2024-06-10 | Dedupe helper function | adelon | |
| 2024-06-05 | Update Megalodon.hs | adelon | |
| 2024-05-22 | Update defaulting for envvar | adelon | |
| 2024-05-22 | Allow `\left` and `\right` everywhere | adelon | |
| 2024-05-21 | Allow line breaks via `\textbox`, handle `\left`/`\right` | adelon | |
| 2024-05-16 | Attach whitespace info to located token | adelon | |
| 2024-05-14 | Update Api.hs | adelon | |
| 2024-05-07 | Update noun guessing | adelon | |
| 2024-05-07 | Sketch noun coord, symbols for reals | adelon | |
| 2024-05-07 | Sketch lexicon mechanism | adelon | |
| 2024-04-01 | Allow numbers in markers (from the second char) | adelon | |
| 2024-03-28 | Allow Windows-style newlines | Simon-Kor | |
| 2024-02-10 | Initial commit | adelon | |
 |
index : naproche-zf.git | |
| Unnamed repository; edit this file 'description' to name the repository. |
| summaryrefslogtreecommitdiff |