Fix term reduce for Host Constants terms

latte-central / latte-kernel

The (very) small kernel of the LaTTe proof assistant

MIT License

11 stars 4 forks source link

Fix term reduce for Host Constants terms #3

Closed zampino closed 5 years ago

zampino commented 5 years ago

Hello @fredokun :-). Maybe I'm getting this totally wrong, by as I was testing out the nice new n-ary prop/and* I got stuck with an exception saying:

Cannot term reduce: unknown (sub-)term {:term :latte-kernel.presyntax/host-constant}

I "accidentally" left a dummy deps.edn file in the PR which will make the project build with clojure tools deps for ease of sharing bleeding edge features, I hope it's fine.

fredokun commented 5 years ago

Thanks, I think it's a nice bugfix, the "host constant" thing is new and still a little bit fragile. I don't mind having a small deps file in the repo. Thanks!