<commit_before>package org.ai4fm.proofprocess.isabelle.core.logic

import isabelle.Term._


/**
 * Various methods to manipulate Isabelle terms.
 * 
 * (adapted from Pure/logic.ML)
 * 
 * @author <NAME>
 */
object Logic {

  private val IMP = "HOL.Trueprop"

  /**
   * A1==>...An==>B  goes to  [A1,...,An], where B is not an implication
   */
  def strip_imp_prems(term: Term): List[Term] = term match {
    case (App(Const(IMP, _), App(a, b))) => a :: strip_imp_prems(b)
    case _ => Nil
  }

  /**
   * A1==>...An==>B  goes to B, where B is not an implication
   */
  def strip_imp_concl(term: Term): Term = term match {
    case (App(Const(IMP, _), App(a, b))) => strip_imp_concl(b)<commit_msg>fixed premises/conclusions splitting<commit_after>package org.ai4fm.proofprocess.isabelle.core.logic

import isabelle.Term._


/**
 * Various methods to manipulate Isabelle terms.
 * 
 * (adapted from Pure/logic.ML)
 * 
 * @author <NAME>
 */
object Logic {

  /**
   * A1==>...An==>B  goes to  [A1,...,An], where B is not an implication
   */
  def strip_imp_prems(term: Term): List[Term] = term match {
    case (App(App(Const("==>", _), a), b)) => a :: strip_imp_prems(b)
    case _ => Nil
  }

  /**
   * A1==>...An==>B  goes to B, where B is not an implication
   */
  def strip_imp_concl(term: Term): Term = term match {
    case (App(App(Const("==>", _), a), b)) => strip_imp_concl(b)
{'fraction_non_alphanumeric': 0.17926565874730022, 'fraction_numerical': 0.005759539236861051, 'mean_word_length': 3.1246290801186944, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 21, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4269187', 'n_tokens_mistral': 548, 'n_tokens_neox': 515, 'n_words': 129}