((((A ∷ ★⁰) ∷ ★⁰) ∷ ★⁰) ∷ ★⁰) (add a cleanup step before pretty printing) #21

Open
opened 2023-07-22 15:20:41 -04:00 by rhi · 1 comment
Owner
No description provided.
rhi added the
ux
label 2023-07-22 15:20:41 -04:00
rhi changed title from ((((A ∷ ★⁰) ∷ ★⁰) ∷ ★⁰) ∷ ★⁰) ⫽ add a cleanup step before pretty printing to ((((A ∷ ★⁰) ∷ ★⁰) ∷ ★⁰) ∷ ★⁰) (add a cleanup step before pretty printing) 2023-08-02 13:32:02 -04:00
Author
Owner

also β redexes, e.g. (λ _ ⇒ Bool) Nat in types of eliminators

also β redexes, e.g. `(λ _ ⇒ Bool) Nat` in types of eliminators
Sign in to join this conversation.
No Milestone
No Assignees
1 Participants
Notifications
Due Date
The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: rhi/quox#21
No description provided.