Commit 2020-09-05 13:51 815a2f97

View on Github →

feat(computability/encoding): define encoding of basic data types (#3976) We define the encoding of natural numbers and booleans to strings for Turing machines to be used in our future PR on polynomial time computation on Turing machines.

Estimated changes

Created src/computability/encoding.lean

added def computability.decode_bool

added theorem computability.decode_encode_bool

added theorem computability.decode_encode_nat

added theorem computability.decode_encode_num

added theorem computability.decode_encode_pos_num

added def computability.decode_nat

added def computability.decode_num

added def computability.decode_pos_num

added def computability.encode_bool

added def computability.encode_nat

added def computability.encode_num

added def computability.encode_pos_num

added theorem computability.encode_pos_num_nonempty

added structure computability.encoding

added def computability.encoding_nat_bool

added def computability.encoding_nat_Γ'

added structure computability.fin_encoding

added def computability.fin_encoding_bool_bool

added def computability.fin_encoding_nat_bool

added def computability.fin_encoding_nat_Γ'

added def computability.inclusion_bool_Γ'

added theorem computability.inclusion_bool_Γ'_injective

added theorem computability.left_inverse_section_inclusion

added def computability.section_Γ'_bool

added theorem computability.unary_decode_encode_nat

added def computability.unary_decode_nat

added def computability.unary_encode_nat

added def computability.unary_fin_encoding_nat

added inductive computability.Γ'