Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Specifically the following Unicode syntax is added and is used by default when pretty-printing:
I × J
(use\x
or\times
) for cube products (ASCII version:I * J
)⊤
(use\top
) for the top tope (ASCII version:TOP
)⊥
(use\bot
) for the bottom tope (ASCII version:BOT
)t ≡ s
(use\equiv
) for point equality tope (ASCII version:t === s
)t ≤ s
(use\leq
or (⌥+<) on macOS) for point inequality tope (ASCII version:t <= s
)φ ∧ ψ
(use\and
) for tope conjunction (ASCII version:phi /\ psi
)φ ∨ ψ
(use\or
) for tope disjunction (ASCII version:phi \/ psi
)A → B
(use\to
) for function types (ASCII version:A -> B
)\ t → s
(use\to
) for lambda abstraction (ASCII version:\ t -> s
)π₁ t
andπ₂ t
(use\pi\1
and\pi\2
) for projections (ASCII versions:first t
andsecond t
)φ ↦ a
(use\mapsto
) for mappings used in extension types andrecOR
(ASCII version:phi |-> a
)*₁
(use\1
) for the only point in the unit cube (ASCII version:*_1
)0₂
(use\2
) for point 0 in the directed interval2
(ASCII version:0_2
)1₂
(use\2
) for point 1 in the directed interval2
(ASCII version:1_2
)The following syntax is NOT added on purpose:
λ x → t
— we want to keepλ
as a valid variable name;The following syntax was already supported but will now also be used by the pretty-printer:
Σ (x : A), B x
(use\Sigma
) for the dependent sum typesThe following syntax is marked as deprecated with warnings issued via
Debug.Trace
:recOR(ψ, φ, a_ψ, a_φ)
is deprecated since the order of arguments is ad hoc; insteadrecOR(ψ ↦ a_ψ, φ ↦ a_φ)
should be used<
and>
) in extension types<{t : I | ψ} → A t [ φ t ↦ a t ]>
is now deprecated (it actually was deprecated since v0.2.0) since it is now a compound type anyway; instead, omit the angle brackets, possibly replacing them with parentheses.