0art0

-- The First-order theory of groups

constant G : Type -- the group
constant m : G × G → G -- the multiplication symbol

notation a `*` b := m (a, b)

-- the group axioms
axiom non_empty : ∃ (g : G), true
axiom mul_assoc : ∀ (a b c : G), m (m (a, b), c) = m (a, m (b, c))

0art0

import tactic

open tactic

/-
Searches for a term `e` in the input list `vars` with type matching `tgt`.
-/
meta def find_term_tgt (tgt : expr) (vars : list expr) : tactic expr :=
  vars.mfirst (λ e,
    do

0art0

/-
An exhaustive description of all possible moves in the game.

Moves of the form `move__nil` are to towers that are empty, while moves of the form
`move__cons` are to towers having at least one disc. The condition of the larger discs being below the
smaller ones is enforced in the latter case.
-/
inductive TowersOfHanoi (n : Nat) : List Nat → List Nat → List Nat → Type _

  | move₁₂nil {a : Nat} {as cs : List Nat} :

0art0

import Lean
import Lean.Elab
import Lean.Elab.Tactic
import Lean.Meta
open Lean Expr Elab Meta Tactic

set_option pp.proofs true
set_option pp.proofs.withType true

/-

0art0

import Aesop

abbrev ℕ := Nat

@[aesop norm unfold]
def InfNat := {f : ℕ → Bool // ∀ n, f n.succ → f n}

namespace InfNat

notation "ℕ∞" => InfNat

0art0

import Lean

open Lean Elab Term Meta Tactic

declare_syntax_cat arith
syntax str : arith
syntax ident : arith
syntax num : arith
syntax arith "+" arith : arith
syntax arith "-" arith : arith