/-
Copyright (c) 2022 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Y. Lewis
-/

import Lean

/-!
A tactic stub file for the `guard_hyp_nums` tactic.
-/

open Lean Meta Elab Tactic

/--
`guard_hyp_nums n` succeeds if there are exactly `n` hypotheses and fails otherwise.

Note that, depending on what options are set, some hypotheses in the local context might
not be printed in the goal view. This tactic computes the total number of hypotheses,
not the number of visible hypotheses.
-/
elab (name := 
guardHypNums: ParserDescr
guardHypNums) "guard_hyp_nums " 
n: ?m.75
n:
num: Parser.Parser
num : 
tactic: Parser.Category
tactic => do
  let 
numHyps: ?m.210
numHyps := 
(← getLCtx): ?m.207
(← 
getLCtx: {m : Type → Type} → [self : MonadLCtx m] → m LocalContext
getLCtx
(← getLCtx): ?m.207
).
size: LocalContext → Nat
size
  
guard: {f : Type → Type ?u.216} → [inst : Alternative f] → (p : Prop) → [inst : Decidable p] → f Unit
guard (
numHyps: ?m.210
numHyps = 
n: ?m.75
n.
getNat: NumLit → Nat
getNat) <|>
    throwError "expected {
n: ?m.75
n.
getNat: NumLit → Nat
getNat} hypotheses but found {
numHyps: ?m.210
numHyps}"