internal exception #3

Stream: lean4

[Aaron Liu]

randomly stumbled into a strange error after copy-pasting a thing wrong

theorem TrivialCohomology.res : NeZero 1 where where
  out := none

[Jovan Gerbscheid]

The list of internal exceptions is

[interrupt,
 postpone,
 unsupportedSyntax,
 abortCommandElab,
 abortTermElab,
 abortTactic,
 autoBoundImplicit,
 isDefEqStuck,
 backtrackFormatter,
 analyzeFailure,
 delabFailure,
 congrHypothesisFailed,
 discrGeneralizationFailure,
 Lean.Meta.LibrarySearch.abortSpeculation,
 checkAssignment,
 outOfScope,
 Aesop.safeExpansionFailedException]

So I presume this isabortCommandElab

[Aaron Liu]

how'd it escape the internals

[Aaron Liu]

and where can I find this internal exception list

[Jovan Gerbscheid]

import Mathlib


open Lean
run_meta do
  let exs ← internalExceptionsRef.get
  logInfo m!"{exs}"