Adding bitvector function definitions to the lean backend

Adding bitvector function definitions to the lean backend #1500