| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-08-27 | working commit | Simon-Kor | |
| 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-24 | naproch sty extension | Simon-Kor | |
 |
index : naproche-zf.git | |
| Unnamed repository; edit this file 'description' to name the repository. |
| summaryrefslogtreecommitdiff |