Boolean expression

[Hu1buerger]

would some kind of boolean expression be possible?

I tried it this way but no luck. Tbh i am not quite sure how the syntax works

true :: true = bool(0)
false :: false = bool(1)
not :: not(true) = false

bool_eq :: bool(A) == bool(B) = A == B

solve :: true == not(false) {
 true | all
 false | all
 bool_eq | all
}

[drocta]

disclaimer: I'm also not confident of my understanding of the syntax, but, just by what the stuff is supposed to do:
I imagine that after running true | all that you would have the expression bool(0) == not(false)
and then after running false | all you would have the expression bool(0) == not(bool(1))
and then bool_eq | all would fail to match anything, because bool(0) == not(bool(1)) is not of the form bool(A) == bool(B).
Instead, I believe you would want to run things in this order (again, I'm unsure of the syntax, and am only commenting on the logic of what you are doing, not the right way to express it syntactically)

someNameGoesHere :: true == not(false) {
    not | all
    true | all
    bool_eq | all
}

so that you would start with true == not(false),
then after not | all you would have true == true,
and then after true | all you would have bool(0) == bool(0)
and then after bool_eq | all you would have 0 == 0 , which I imagine is what you were trying to get.
(I believe all of the | all in what I said, other than the true | all, could be replaced with | 0 because there is only one place where it applies.)

(I don't know whether == is an allowed infix operator in this language)

[wiebecommajonas]

Boolean expressions are entirely possible., but like @drocta mentioned, you will have to drop the == operator for now.

And because Noq does not support conditional rule application (yet), you will have to do it manually.

Here I wrote a short example of what it could look like:

and_f :: and(bool(false), bool(_)) = bool(false)
and_t :: and(bool(true), bool(true)) = bool(true)

or_f :: or(bool(false), bool(false)) = bool(false)
or_t :: or(bool(true), bool(_)) = bool(true)

not_f :: not(bool(false)) = bool(true)
not_t :: not(bool(true)) = bool(false)
not_and :: not(and(bool(A), bool(B))) = or(not(A), not(B))
not_or :: not(or(bool(A), bool(B))) = and(not(bool(A)), not(bool(B)))

eq_f :: eq(bool(true), bool(false)) = bool(false)
eq_t :: eq(bool(A), bool(A)) = bool(true)

basic_comm :: B(X, Y) = B(Y, X)

eq(bool(true), bool(false)) {
	eq_f | all
}

eq(and(bool(false), bool(true)), bool(false)) {
	and_f | all
	eq_t | all
}

eq(not(or(bool(false), bool(true))), and(not(bool(true)), bool(true))) {
    not_or | all
    not_f | all
    not_t | all
    basic_comm | 1
    and_f | all
    eq_t | all
}