AngouriMath

Navigation

Home Quick start Wiki Almanac Research What's new Try Use Angouri.org GitHub Report a bug Donate Contacts

AngouriMath

← Back to list of namespaces

Classes within the AngouriMath namespace

• Entity

  Summary

  This is the main class in AngouriMath.
  Every node, expression, or number is an Entity.
  However, you cannot create an instance of this class, look for the nested classes instead.
  

• EntityEvaluationExtension

• InternalAMExtensions

  Summary

  This is a set of extensions for internal use. You might be more interested
  in publicly exposed AngouriMathExtensions or function class MathS

• MathS

  Summary

  Use functions from this class

• ProofRecording

  Summary

  A scope that collects the steps by which the quantified statements decided inside it were
  decided, the way RewriteRecording collects rewrites: the proof of
  forall n in ZZ+ : sum(k, k, 1, n) = n (n + 1)/2 is the closed form read through
  its case, the proof of forall n in ZZ+ : sum(1/(k (k + 1)), k, 1, n) = n/(n + 1) is a base case and a step, each a step here. Nothing is collected outside a scope, and
  the ordinary path does not pay for one nobody opened. A decision already made is not
  made again: an entity whose Evaled is cached, or a statement parsed
  through the parser's cache and evaluated before, records nothing, so a proof is asked of
  a fresh entity (FromString(System.String,System.Boolean) with the cache off).
  

  Example

  using var proof = ProofRecording.Start();
  var verdict = "forall n in ZZ+ : sum(1/(k (k + 1)), k, 1, n) = n/(n + 1)".ToEntity().Evaled;
  foreach (var step in proof.Steps)
      Console.WriteLine(step);

• ProofStep

  Summary

  One step in the decision of a quantified statement: the statement that was decided, the
  rule that decided it, the verdict, and how deep it sits under the statement asked --
  the base case of an induction is one below the induction, the identity that settles the
  step one below that. The rule is named as the reference names it and as a checker
  would: Lemma is the Lean 4 tactic or lemma the step corresponds to, which
  is what an export to a proof checker needs and the design constraint of
  #746's proof engine.
  #1409