I renamed `in_neg_norm`

to `in_nnf`

to be less confusing.

It would probably be better practice to return an `nnf_form`

type instead that inherently shows only literals can have a negation sign now that I think a little more on it.

I rewrote it like I mentioned, but now I wonder if Coq allows me to make the notation a bit prettier. In particular it would be awesome if it could parse `<[ sym ]>`

as `NVar sym false`

. I only managed to get it working for the negated variant.

```
Inductive nnf_form: Type :=
| NVar (sym: string) (sign: bool)
| NTrue
| NFalse
| NAnd (p q: nnf_form)
| NOr (p q: nnf_form).
(* Declare notation to simplify working with nnf formulas. *)
Declare Custom Entry sat_nnf.
Declare Scope sat_nnf_scope.
Declare Custom Entry sat_nnf_aux.
Notation "<[ e ]>" := e (e custom sat_nnf_aux) : sat_nnf_scope.
Notation "e" := e (in custom sat_nnf_aux at level 0, e custom sat_nnf) : sat_nnf_scope.
Notation "( x )" := x (in custom sat_nnf, x at level 99) : sat_nnf_scope.
Notation "x" := x (in custom sat_nnf at level 0, x constr at level 0) : sat_nnf_scope.
Notation "'true'" := NTrue (in custom sat_nnf at level 0).
Notation "'false'" := NFalse (in custom sat_nnf at level 0).
Notation "~ x" := (NVar x true) (in custom sat_nnf at level 5, right associativity).
Notation "p /\ q" := (NAnd p q) (in custom sat_nnf at level 10, left associativity).
Notation "p \/ q" := (NOr p q) (in custom sat_nnf at level 15, left associativity).
Open Scope sat_nnf_scope.
```

Last updated: Jun 13 2024 at 19:02 UTC