search

FormalSAT / trestle

Apache License 2.0
17 stars 2 forks source link

Require mathlib and define propositional formulas #4

Closed Vtec234 closed 11 months ago

Vtec234 commented 11 months ago

A little warmup PR. We require mathlib, define propositional formulas, entailment, and equivalence. (I also snuck in a Nix flake if that's alright.)

@JamesGallicchio I understand you wanted main protected? I am making this PR against a new dev branch for that.

Vtec234 commented 11 months ago

Btw, this pulls in mathlib universally. We could start by making a separate package instead as discussed. Thoughts?

JamesGallicchio commented 11 months ago

ATM I'm the only downstream user of this lib, so the unilateral mathlib dependency is fine. No reason to make more work for ourselves right now.