Alternate mathy syntax #15

New issue

Open

opened 2024-12-05 19:37:05 -08:00 by wball · 0 comments

wball commented

2024-12-05 19:37:05 -08:00

Owner

I've had a bunch of ideas for a more mathematician-friendly syntax bouncing around my head for a while. I'm envisioning something like

Theorem basic (S : *) (P : S → *) :
    (∀ (x : S), P x → Q x) → (∀ (x : S), P x) → ∀ (x : S), Q x.
Proof
        1. Suppose ∀ (x : S), P x → Q x
        2. Suppose ∀ (x : S), P x
        3. Let x : S
        4. P x by [2 x]
        5. Q x by [1 x 4]
Qed

but I haven't thought it through all the way. Support for equational reasoning and more structured proofs would be a must as well, but I haven't quite thought through how that would work.

I've had a bunch of ideas for a more mathematician-friendly syntax bouncing around my head for a while. I'm envisioning something like ``` Theorem basic (S : *) (P : S → *) : (∀ (x : S), P x → Q x) → (∀ (x : S), P x) → ∀ (x : S), Q x. Proof 1. Suppose ∀ (x : S), P x → Q x 2. Suppose ∀ (x : S), P x 3. Let x : S 4. P x by [2 x] 5. Q x by [1 x 4] Qed ``` but I haven't thought it through all the way. Support for equational reasoning and more structured proofs would be a must as well, but I haven't quite thought through how that would work.