Welcome to SWI-Prolog (threaded, 64 bits, version 9.0.4)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.

For online help and background, visit https://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).

?- trace.
true.

[trace]  ?- ti(Τ), ⊢ M : Τ.
   Call: (11) ti(_2934) ?
   Exit: (11) ti(α⇒α) ?
   Call: (11) ⊢_2938:α⇒α ?
   Call: (12) []⊢_2938:α⇒α ?
   Call: (13) isvar(_2938) ?
   Call: (14) atom(_2938) ?
   Fail: (14) atom(_2938) ?
   Fail: (13) isvar(_2938) ?
   Redo: (12) []⊢_2938:α⇒α ?
   Call: (13) [_9378:α]⊢_9380:α ?
   Call: (14) isvar(_9380) ?
   Call: (15) atom(_9380) ?
   Fail: (15) atom(_9380) ? a

[trace]  ?- notrace.
true.

[debug]  ?- nodebug.
true.

?- ti(Τ), ⊢ M : Τ.
Τ = α⇒α,
M = λ(_A, _A)

?- tk(Τ), ⊢ M : Τ.
Τ = α⇒β⇒α,
M = λ(_A, λ(_, _A))

?- ts(Τ), ⊢ M : Τ.
  C-c C-cAction (h for help) ? a
abort
% Execution Aborted

?- nat(Τ), ⊢ M : Τ.
Τ = (α⇒α)⇒α⇒α,
M = λ(_A, _A) ;
Τ = (α⇒α)⇒α⇒α,
M = λ(_, λ(_A, _A)) ;
Τ = (α⇒α)⇒α⇒α,
M = λ(_A, λ(_B, app(_A, _B))) ;
Τ = (α⇒α)⇒α⇒α,
M = λ(_A, λ(_B, app(_A, app(_A, _B)))) ;
Τ = (α⇒α)⇒α⇒α,
M = λ(_A, λ(_B, app(_A, app(_A, app(_A, _B))))) ;
Τ = (α⇒α)⇒α⇒α,
M = λ(_A, λ(_B, app(_A, app(_A, app(_A, app(_A, _B))))))

?- ts(Τ), ⊢ M : Τ.
Τ = (α⇒β⇒γ)⇒(α⇒β)⇒α⇒γ,
M = λ(_A, λ(_B, λ(_C, app(app(_A, _C), app(_B, _C)))))

?- tab(Τ), ⊢ M : Τ.
false.

?- ⊢ M : α.
false.

?- true.

?- ty(Τ), ⊢ M : Τ.
  C-c C-cAction (h for help) ? a
abort
% Execution Aborted

?- ty(Τ), ⊢ M : Τ.
false.

?- ⊢ M : (α ⇒ β) ⇒ (β ⇒ α) ⇒ β.
false.

?- nat(Τ), ⊢ M : Τ.
Τ = (α⇒α)⇒α⇒α,
M = λ(_, λ(_A, _A)) ;
false.

?- nat(Τ), ⊢ M : Τ.
Τ = (α⇒α)⇒α⇒α,
M = λ(_, λ(_A, _A)) ;
false.

?-