Open bash opened 1 year ago
If a normal form exists, annotate it with a list of nominal definitions it matches.
E.g. for the following term:
True -> (&t f . t) False -> (&t f . f) 0 --> (&f x. x) (False)
The normal form should be shown as:
->> (λ(λ1)) ^^^^^^^ Also known as False, 0.
If a normal form exists, annotate it with a list of nominal definitions it matches.
E.g. for the following term:
The normal form should be shown as: