- A Programming Language with Higher-Order Logic
stack ghci
ghci> Main.main
colorable=True
Hol =<< Example/stlc.hol
Hol> Compiling Example.stlc ( Example/stlc.hol, interpreted )
Example.stlc> Ok, one module loaded.
Example.stlc> ?- check (lam x\ x) T.
Example.stlc> The answer substitution is:
Example.stlc> T := fn ?V_441 ?V_441.
Example.stlc> Find more solutions? [Y/n] Y
Example.stlc> no.
Example.stlc> :q
Hol >>= quit