khoek

import data.string data.list.defs
import tactic.core

def {u v w} list.mfilter_map {m : Type u → Type v} [alternative m] [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m (list β)
| []       := return []
| (h :: t) := do h' ← (f h >>= λ v, pure $ list.cons v []) <|> pure [],
                 t' ← list.mfilter_map t,
                 return (h' ++ t')

namespace tactic

khoek

import data.string
import tactic.core

namespace tactic

private meta def attempt_instance_build (n : name) (ns : list name) : tactic unit :=
do sorries ← ns.mmap $ λ _, to_pexpr <$> mk_sorry,
   let s : structure_instance_info := {
       struct := some n,
       field_names := ns,

khoek

open tactic

namespace tactic

meta inductive semigroup_expr
| atom (e : expr) 
| mul (l r : semigroup_expr)

namespace semigroup_expr

khoek

open tactic

namespace tactic

meta inductive semigroup_expr
| atom (e : expr) 
| mul (l r : semigroup_expr)
namespace semigroup_expr

meta def eval : semigroup_expr → tactic expr