Module prop::path_semantics
source[−]Expand description
Path Semantics
Path Semantics has a core axiom which is used to model mathematics.
This core axiom is modelled here, lifting proof of path semantical order to expressions of propositions.
For more information, see https://github.com/advancedresearch/path_semantics.
Re-exports
pub use quality::Q;
pub use quality::self_quality_left as refl_left;
pub use quality::self_quality_right as refl_right;
Structs
Traits
Shorthand for decidable proposition with path semantical level.
Path semantical proposition level.
Look by index.
Path semantical order.
Sorts two types.
Sorts two types.
Functions
Assumes the core axiom safely for propositions.
Generates naive core axiom at increased path semantical proposition level.
Assume naive core axiom safely.
Assume a normalised naive core axiom.
Generates a naive core axiom which has reflection as end-lines.
Checks that X
is qual to T
.
Composition.
Checks whether two proposition levels are equal.
Checks whether a proposition level is less than another.
Composition using the naive core axiom.
Reduce naive core axiom in case of false to equality of associated propositions.
Use both PAndFst
and PAndSnd
to prove a = b
.
Converts to naive core axiom.
Converts core axiom to PAndFst
.
Converts core axiom to PAndSnd
.
Converts core axiom to POrFst
.
Converts core axiom to POrSnd
.
Proves that types are unique.
Use both PAndFst
and PAndSnd
.
Constructs a 2D naive core axiom from two naive core axioms, where one is normalised of the other.
Type Definitions
Increases level one step.
Increases proposition level of A
with some amount N
.
Look up type N
among the normalised A, B, C, D
.
Returns the maximum LProp.
The decided maximum (4th of 4).
The undecided maximum minimum.
The decided maximum of undecided middle (3rd of 4).
Returns the minimum LProp.
The undecided minimum maximum.
The decided minimum (1st of 4).
The decided minimum of undecided middle (2nd of 4).
Normalise 4 LProp
s (sorted ascending by propositional level).
Sends first argument of Logical AND to higher level.
Sends second argument of Logical AND to higher level.
Sends first argument of Logical OR to higher level.
Sends second argument of Logical OR to higher level.
Core axiom of Path Semantics.
Naive axiom of Path Semantics (without order assumption).
Normalised naive core axiom.