Method push

crates/kernel/src/lctx.rs:109–113

Push a declaration. The caller is responsible for ensuring `id` is fresh (typically from [`NameGenerator::fresh`]).

(&mut self, id: FVarId, decl: LocalDecl<M>)

  /// Push a declaration. The caller is responsible for ensuring `id` is
  /// fresh (typically from [`NameGenerator::fresh`]).
  pub fn push(&mut self, id: FVarId, decl: LocalDecl<M>) {
    let pos = self.decls.len();
    self.decls.push((id, decl));
    self.index.insert(id, pos);
  }

  /// Truncate the context to the given length, dropping any declarations
  /// pushed since. The dropped fvars become unresolvable via [`Self::find`].