original_docstring: 
          Check if the term can be proven to have the given typecode,
          without producing any proof
          
docstring: Check if the term can be proven to have the given typecode,
  without producing any proof
docstring_tokens: Check if the term can be proven to have the given typecode without producing any proof
code: def check_typecode(
          composer: Composer,
          typecode: str,
          term: Term,
          # allow extra typecode check
          extension: Optional[Callable[[str, Term], bool]] = None,
      ) -> bool:
          """
          Check if the term can be proven to have the given typecode,
          without producing any proof
          """
          # try to find a matching floating statement first if the term is a metavariable
          if isinstance(term, Metavariable):
              for theorem in composer.get_theorems_of_typecode(typecode):
                  if isinstance(theorem.statement, FloatingStatement):
                      _, metavar = theorem.statement.terms
                      assert isinstance(metavar, Metavariable)
  
                      if metavar.name == term.name:
                          return True
              # otherwise treat the metavariable as a term
  
          # try to find a non-floating statement without hypotheses and unify
          for theorem in composer.get_theorems_of_typecode(typecode):
              if (len(theorem.context.essentials) <= 1 and not isinstance(theorem.statement, FloatingStatement)
                      and len(theorem.statement.terms) == 2):
                  # check that expected_statement is an instance of theorem.statement
                  solution = Unification.match_terms_as_instance(theorem.statement.terms[1], term)
                  if solution is None:
                      continue
  
                  for floating in theorem.context.floatings:
                      if not TypecodeProver.check_typecode(composer, floating.typecode, solution[floating.metavariable],
                                                           extension=extension):
                          break
                  else:
                      return True
  
          if extension is not None:
              return extension(typecode, term)
  
          return False
code_tokens: def check_typecode ( composer : Composer , typecode : str , term : Term , extension : Optional [ Callable [ [ str , Term ] , bool ] ] = None , ) -> bool : if isinstance ( term , Metavariable ) : for theorem in composer . get_theorems_of_typecode ( typecode ) : if isinstance ( theorem . statement , FloatingStatement ) : _ , metavar = theorem . statement . terms assert isinstance ( metavar , Metavariable ) if metavar . name == term . name : return True for theorem in composer . get_theorems_of_typecode ( typecode ) : if ( len ( theorem . context . essentials ) <= 1 and not isinstance ( theorem . statement , FloatingStatement ) and len ( theorem . statement . terms ) == 2 ) : solution = Unification . match_terms_as_instance ( theorem . statement . terms [ 1 ] , term ) if solution is None : continue for floating in theorem . context . floatings : if not TypecodeProver . check_typecode ( composer , floating . typecode , solution [ floating . metavariable ] , extension = extension ) : break else : return True if extension is not None : return extension ( typecode , term ) return False
short_docstring: Check if the term can be proven to have the given typecode,
  without producing any proof
short_docstring_tokens: Check if the term can be proven to have the given typecode without producing any proof
comment: # allow extra typecode check$SEP$"""
          Check if the term can be proven to have the given typecode,
          without producing any proof
          """$SEP$# try to find a matching floating statement first if the term is a metavariable$SEP$# otherwise treat the metavariable as a term$SEP$# try to find a non-floating statement without hypotheses and unify$SEP$# check that expected_statement is an instance of theorem.statement