Illegal begin of top_parse

jrh13 / hol-light

The HOL Light theorem prover

Other

435 stars 79 forks source link

Open AI-coder opened 4 years ago

AI-coder commented 4 years ago

When I input " 'x+1' " in hol-light system , it responses "Illegal begin of top_parse", whats wrong with it ?, Thanks.

maggesi commented 4 years ago

Use backquote ` not single quote ' (apostrophe)

`x+1`