Documentation

Lean.Meta.CasesOn

Instances For

    Return some c if e is a casesOn application.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Convert c back to Expr

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Given a casesOn application c of the form

        casesOn As (fun is x => motive[i, xs]) is major  (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
        

        and an expression e : B[is, major], construct the term

        casesOn As (fun is x => B[is, x] → motive[i, xs]) is major (fun ys_1 (y : B[C_1[ys_1]]) => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n (y : B[C_n[ys_n]]) => (alt_n : motive (C_n[ys_n]) e remaining
        

        We use kabstract to abstract the is and major from B[is, major].

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Similar CasesOnApp.addArg, but returns none on failure.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For