Module prop::path_semantics[−][src]

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.

LTrue	True for a path semantical level.
POrdProof	Proof of path semantical order.

DLProp	Shorthand for decidable proposition with path semantical level.
LProp	Path semantical proposition level.
Lookup	Look by index.
PBinOrd	Path semantical order for binary operators.
POrd	Path semantical order.
SortMax	Sorts two types.
SortMin	Sorts two types.

assume ^⚠	Assumes the core axiom for propositions.
assume_inc_path_level	Generates naive core axiom at increased path semantical proposition level.
assume_norm_path_level	Assume a normalised naive core axiom.
assume_path_level	Generates naive core axiom using assumption on path semantical proposition levels.
assume_path_refl	Generates a naive core axiom which has reflection as end-lines.
comp	Composition.
eq_lev	Checks whether two proposition levels are equal.
lt_lev	Checks whether a proposition level is less than another.
naive_comp	Composition using the naive core axiom.
naive_red_false	Reduce naive core axiom in case of false to equality of associated propositions.
pand_both_eq	Use both `PAndFst` and `PAndSnd` to prove `a = b`.
pand_join	Join `PAndFst` and `PAndSnd`.
path_level	Converts to naive core axiom using path semantical proposition levels.
red_false	Reduce core axiom in case of false to equality of associated propositions.
to_pand_fst	Converts core axiom to `PAndFst`.
to_pand_snd	Converts core axiom to `PAndSnd`.
uniq_ty	Proves that types are unique.
use_pand_both	Use both `PAndFst` and `PAndSnd`.

IncLevel	Increases proposition level of `A` with some amount `N`.
LN	Look up type `N` among the normalised `A, B, C, D`.
Max	Returns the maximum LProp.
MaxMax	The decided maximum (4th of 4).
MaxMin	The undecided maximum minimum.
Maxi	The decided maximum of undecided middle (3rd of 4).
Min	Returns the minimum LProp.
MinMax	The undecided minimum maximum.
MinMin	The decided minimum (1st of 4).
Mixi	The decided minimum of undecided middle (2nd of 4).
Normalise	Normalise 4 `LProp`s (sorted ascending by propositional level).
PAnd	Sends Logical AND to higher level.
PAndFst	Sends first argument of Logical AND to higher level.
PAndSnd	Sends second argument of Logical AND to higher level.
PSem	Core axiom of Path Semantics.
PSemNaive	Naive axiom of Path Semantics (without order assumption).
PSemNaiveNorm	Normalised naive core axiom.