search

aya-prover / aya-prover-proto

┗:smiley:┛ ┏:smiley:┓ ┗:smiley:┛
GNU General Public License v3.0
11 stars 0 forks source link

Finish Parser #59

Closed imkiva closed 3 years ago

imkiva commented 3 years ago

Progress of the parser:

Things to be addressed:

Originally posted in #54

ice1000 commented 3 years ago

Tbh I think pi can really improve readability, but I don't think that's necessary (see how things work out in Agda. You'll have \forall and \exists anyway because these two are different)

re-xyr commented 3 years ago

Tbh I think pi can really improve readability, but I don't think that's necessary (see how things work out in Agda. You'll have \forall and \exists anyway because these two are different)

That’s absolutely OK, just make it optional as we discussed (if it won’t bring any difficulties to parsing).

tonyxty commented 3 years ago

Tbh I think pi can really improve readability, but I don't think that's necessary (see how things work out in Agda. You'll have \forall and \exists anyway because these two are different)

Agreed. And I think we should make them mandatory.

ice1000 commented 3 years ago

Tbh I think pi can really improve readability, but I don't think that's necessary (see how things work out in Agda. You'll have \forall and \exists anyway because these two are different)

Agreed. And I think we should make them mandatory.

You mean \Pi or \forall?

ice1000 commented 3 years ago

Are we not going to allow A -> B without \Pi prefix?

ice1000 commented 3 years ago

Also, what's left to be done in Mzi.g4? I think we're almost all set apart from small polishment (sorry for using weird words, I just can't control).

ice1000 commented 3 years ago

I ain't joking woman I got to ramble

imkiva commented 3 years ago

Also, what's left to be done in Mzi.g4? I think we're almost all set apart from small polishment (sorry for using weird words, I just can't control).

record, codata and some grammar sugar in Foundations.mzi.

Are we going to support them?

imkiva commented 3 years ago

Are we not going to allow A -> B without \Pi prefix?

Vote:

re-xyr commented 3 years ago

I still stand firmly by being optional

tonyxty commented 3 years ago

Tbh I think pi can really improve readability, but I don't think that's necessary (see how things work out in Agda. You'll have \forall and \exists anyway because these two are different)

Agreed. And I think we should make them mandatory.

You mean \Pi or \forall?

I mean we don't allow bare (x : A) -> B x syntax

ice1000 commented 3 years ago

Also, what's left to be done in Mzi.g4? I think we're almost all set apart from small polishment (sorry for using weird words, I just can't control).

record, codata and some grammar sugar in Foundations.mzi.

Are we going to support them?

Not now. We're far from then, I guess

ice1000 commented 3 years ago

Are we not going to allow A -> B without \Pi prefix?

Vote:

  • ❤️ for making \Pi optional
  • 👀 for making \Pi obligatory

Seems my vote will be crucial. I think we can make it mandatory for now, and do some little research on other proof assistants' way, like lean or coq or f* or whatever. Maybe you'll discover something new about yourself.

ice1000 commented 3 years ago

@OlingCat @xiaoxiangmoe maybe sharing your ideas?