Well yes, either direct input or wider context (i.e. environment, library). You can only construct values for tautology types with expressions not referring to context.
Well yes, either direct input or wider context (i.e. environment, library). You can only construct values for tautology types with expressions not referring to context.