search

JetBrains / arend-lib

Apache License 2.0
79 stars 23 forks source link

Add metas for \Pi, similar to metas for \Sigma #35

Closed marat-rkh closed 2 years ago

marat-rkh commented 3 years ago

For TruncP (\Sigma (x : A) B) we can write ∃ (x : A) B or ∃ {x} B. It would be nice to have an ability to write ∀ (x : A) B or ∀ {x} B for \Pi (x : A) B when B : A -> \Prop.

valis commented 3 years ago

For \exists it makes sense because it is actually doing something, it adds TruncP, but \forall is just a synonym for \Pi

marat-rkh commented 3 years ago

This is true, it would be a synonym. But I believe it could increase readability when you encode logic, especially when you have both ∃ and ∀ in one formula. Also, as far as I understand, you cannot drop : A from \Pi (a : A) B, so ∀ {x} B could be handy.

marat-rkh commented 2 years ago

Fixed in https://github.com/JetBrains/arend-lib/commit/c74cdddb38fab881da4b82c1f660603de02680e6