Documentation

>>> demo_ basicCtx ("Boo" :: Term LambdaStar)
error:
• Variable not in scope Boo

>>> demo_ basicCtx (lam_ "x" "x" -:- "Bool" :: Term STLC)
error:
• The lambda expression λ x → x doesn't have a Pi-type
• Annotated with Bool
• when checking expression
  λ x → x : Bool

>>> demo_ basicCtx ("True" @@ "False" :: Term LambdaStar)
error:
• Couldn't match actual type Bool with a function type
• In the application of True
• to the value False
• when checking expression
  True False

If we try to apply variable to variable values, it's ok however. We can be weird, so True is actually a function:

>>> prettyPut ("True" @@ "False" :: Value LambdaStar)
True False

Yet, if we apply to a sort, or Pi-type or something else obviously incorrect: value will fail:

>>> prettyPut (sort_ LambdaStar `valueApp` "False" :: Value LambdaStar)
panic 'apply': Trying to apply not-a-lambda ⋆

We don't print a value we try to apply, because it's still not evaluated. (often some variable in a scope).