module
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSCarrier
show as:
view Lean formalization →
used by (3)
depends on (2)
declarations in this module (14)
-
inductive
FRSExpr -
def
eval -
theorem
eval_mem -
theorem
rat_is_term -
theorem
phi_is_term -
theorem
pi_is_term -
theorem
e_is_term -
theorem
alphaInv_is_term -
def
carrierValues -
theorem
carrierValues_subset -
theorem
carrierValues_countable -
theorem
carrierValues_proper -
theorem
has_protocol_display -
theorem
frs_carrier