User:Octogeddonling

hi i'm here.

The Prove-it Language

Prove-it Language is a bruh language to use. Its boolean value has 3 values: True, False, and Undecided. Only former 2 will be used in the definition but the third one may pop out in the action part.

The code can be divided into two parts: define and act, a "act" line is inserted between.

The defined functions in definition part are add 1(+(x)), and(&(x,y)), or(|(x,y)), not(!(x)). All things with a input is seen as a function but a number as a function will always return equation. All functions in the defined part returns only Boolean values. The only defined value is 0.

At the start of the define part, you can state which are global variables(eg. a and b) by typing var a b. the variables are default natural numbers and they can be used and re-valued in the action part.

In the defined part, you write mathematical statements by typing non-stated variable and they are "for all of ... the expression holds"(eg: x ...). Be wary to not type a contradiction because this will be a syntax error. Everything is by default a predicate and adding 1 makes all number value shift by 1 while the new 0 is default false. eg: if you have a isEven and +(isEven) returns whether it's odd.

Now to the action part. There are S, K in SKI calculus, and a unitary print() function that can print natural numbers(or the minimum natural number meeting some predicate, null when it's always false). Converting them to binary and to strings maybe? The action part is completely different from definition part and the only common is global variables.