datokrat

module

public meta import Lean

open Lean Elab Tactic Meta Simp Tactic.TryThis

namespace MinimizeSimps

/-- Check if a syntax node is a `simp only` call (simp, simp_all, or dsimp with `only`). -/
private meta def isSimpOnlyNode (stx : Syntax) : Bool :=

datokrat

module

prelude
public meta import Lean.Elab.Eval
public import Init

public section

namespace Lean.Parser.Term

datokrat

import Lean

open Lean Meta Elab Tactic

/-! # `defeq_abuse_locs` tactic
For each function application in the goal's target expression, determines the
*expected type* (parameter type from the function) and the *inferred type*
(actual type of the argument). Then checks at which transparency modes these
are definitionally equal.
Collects all (argument, expected, inferred) triples that require more than

datokrat

import Lean

open Lean Meta Elab Tactic

/-! # `defeq_abuse_score` tactic
Checks at which transparency level the current goal's target expression type-checks.
Reports a numeric "defeq abuse score":
- 0: typechecks at `reducible` (no defeq abuse)
- 1: typechecks at `instances` (mild — needs instance unfolding)
- 2: typechecks at `default` (moderate — needs default unfolding)

datokrat

export function just<T>(value: T): Just<T> {
  return new _Just<T>(value) as Just<T>;
}

export function nothing(): Nothing<any> {
  return new _Nothing() as Nothing<any>;
}

export interface MBase<T> {
  type: "just" | "nothing";

datokrat

Keybase proof

I hereby claim:

• I am datokrat on github.
• I am datokrat (https://keybase.io/datokrat) on keybase.
• I have a public key whose fingerprint is 28C3 6142 A24C 1ED3 F5AC BDDF 2437 162C 4747 1BEF

To claim this, I am signing this object: