Will it support conditional rule? Like when x is invertible than we can apply x*x^-1 = 1, it will convenience because i want use Noq to calculate some advanced algebra(i think it is very useful for working mathematicians), for example, i want it applies proper base change in Algebraic Geometry just to the morphism which is proper, but i don't want to apply it everywhere(which will mess up everything), In this situation, i don't mean a proof assistant, but just a lightweight mark to control the rules' application.(because you still don't need to prove this can be applied)
Will it support conditional rule? Like when
xis invertible than we can applyx*x^-1 = 1, it will convenience because i want use Noq to calculate some advanced algebra(i think it is very useful for working mathematicians), for example, i want it applies proper base change in Algebraic Geometry just to the morphism which is proper, but i don't want to apply it everywhere(which will mess up everything), In this situation, i don't mean a proof assistant, but just a lightweight mark to control the rules' application.(because you still don't need to prove this can be applied)