Closed gburel closed 1 year ago
New options -lp and -lpterm for lambdapi output, -dk and -dkterm are reverted to what they do in the modulo branch. -lpterm now rewrites a symbol corresponding to the goal defined in the signature, instead of defining an hard-coded delta symbol.
New options -lp and -lpterm for lambdapi output, -dk and -dkterm are reverted to what they do in the modulo branch. -lpterm now rewrites a symbol corresponding to the goal defined in the signature, instead of defining an hard-coded delta symbol.