MCPcopy Create free account

hub / github.com/agenticsorg/lean-agentic / functions

Functions1,015 in github.com/agenticsorg/lean-agentic

↓ 347 callersMethodlog
* Log message to stderr (for debugging, not protocol communication)
npm/lean-agentic/mcp/server.js:258
↓ 112 callersMethodpush
Push a new binding
leanr-elab/src/context.rs:39
↓ 90 callersMethodclone
(&self)
runtime/src/mailbox.rs:146
↓ 74 callersMethodclone
(&self)
lean-agentic/src/environment.rs:302
↓ 47 callersMethodlen
(&self)
runtime/src/mailbox.rs:93
↓ 40 callersMethodadvance
Advance to next character
leanr-syntax/src/lexer.rs:425
↓ 39 callersMethodmk_var
Create a variable term
lean-agentic/src/arena.rs:130
↓ 37 callersMethodinsert
Insert WHNF result
leanr-eval-lite/src/cache.rs:36
↓ 34 callersMethodmk_app
Create an application term
lean-agentic/src/arena.rs:135
↓ 31 callersMethodadvance
Advance to next token
leanr-syntax/src/parser.rs:692
↓ 28 callersMethodcheck
Check if current token matches
leanr-syntax/src/parser.rs:667
↓ 28 callersMethodget
Get a term by its ID
lean-agentic/src/arena.rs:75
↓ 26 callersMethodprocess
Process a RAG query with policy verification
leanr-rag-gateway/src/lib.rs:109
↓ 24 callersMethodexpect
Expect a specific token
leanr-syntax/src/parser.rs:675
↓ 22 callersMethodcreateVariable
* Demonstrate hash-consing: creating same term twice reuses memory * Returns true if successful * @param {number} index * @returns {boo
npm/lean-agentic/wasm-web/leanr_wasm.js:157
↓ 22 callersMethodmk_sort
Create a sort term
lean-agentic/src/arena.rs:116
↓ 21 callersMethodintern
Intern a term and return its ID
lean-agentic/src/arena.rs:45
↓ 20 callersMethodinsert
( &self, id: &str, vector: &[f32], payload: HashMap<String, serde_json::Value>
src/agentdb/vector_store.rs:128
↓ 20 callersMethodkind
Get the kind of a term by its ID
lean-agentic/src/arena.rs:85
↓ 18 callersMethodparse_expr
Parse an expression
leanr-syntax/src/parser.rs:317
↓ 17 callersMethodspan
Get the span of this expression
leanr-syntax/src/ast.rs:207
↓ 17 callersMethodto
Combine two spans into a single span covering both
leanr-syntax/src/span.rs:35
↓ 15 callersFunctionspawn
1. Spawn: Create new agent (<500ns target)
runtime/src/orchestration.rs:54
↓ 15 callersMethodspawn
Spawn a new agent
runtime/src/runtime.rs:70
↓ 15 callersMethodstart
Start the runtime
runtime/src/runtime.rs:46
↓ 15 callersMethodzero
Get the zero level ID
lean-agentic/src/level.rs:116
↓ 14 callersFunctioncreateDemo
()
npm/lean-agentic/src/web.js:90
↓ 14 callersMethodcurrent_char
Get current character
leanr-syntax/src/lexer.rs:415
↓ 14 callersMethodinit
* Initialize AgentDB connection
npm/lean-agentic/src/agentdb-integration.js:37
↓ 14 callersMethodmk_nat
Create a natural number literal
lean-agentic/src/arena.rs:165
↓ 14 callersMethodrecv
Receive message (async)
runtime/src/mailbox.rs:116
↓ 14 callersMethodstop
Stop the runtime
runtime/src/runtime.rs:58
↓ 13 callersMethodgetStats
()
npm/lean-agentic/src/web.js:70
↓ 13 callersMethodintern
Intern a term into the hash-consed arena This computes the canonical representative [t]≡ ∈ T̂ Complexity: O(1) amortized
leanr-theorems/src/hashcons_confluence.rs:79
↓ 13 callersMethodparse_ident
Parse an identifier
leanr-syntax/src/parser.rs:651
↓ 12 callersMethodadd_episode
Add an episode to memory
examples/memory-copilot/explainable_memory.rs:98
↓ 12 callersFunctioncreate_test_episode
(id: &str, content: &str, entities: Vec<String>)
examples/memory-copilot/explainable_memory.rs:351
↓ 12 callersMethoddemonstrateHashConsing
()
npm/lean-agentic/src/web.js:60
↓ 12 callersMethodlen
Get the length of this span
leanr-syntax/src/span.rs:45
↓ 12 callersMethodmax
Create a max level
lean-agentic/src/level.rs:136
↓ 12 callersMethodsend
Send message with backpressure check Returns error if above high water mark.
runtime/src/mailbox.rs:168
↓ 12 callersMethodstats
Get cache statistics (demonstrates hash-consing benefit)
leanr-theorems/src/confluence.rs:145
↓ 11 callersMethodcreateIdentityFunction
* Create a lambda abstraction (x : Type) => x * @returns {boolean}
npm/lean-agentic/wasm-web/leanr_wasm.js:198
↓ 11 callersMethodget_mut
(&mut self)
runtime/src/capabilities.rs:101
↓ 11 callersMethodmk_const
Create a constant term
lean-agentic/src/arena.rs:121
↓ 11 callersMethodmk_lam
Create a lambda term
lean-agentic/src/arena.rs:140
↓ 11 callersMethodparallel_reduce
Compute parallel reduction of a term This is a single-step reduction that reduces ALL β-redexes simultaneously. For example: - `(λx.x) ((λy.y) z)` ⇉
leanr-theorems/src/confluence.rs:83
↓ 11 callersFunctiontest
* Test helper
npm/lean-agentic/tests/theorems/basic-theorems.test.js:27
↓ 11 callersMethodupdate
Update profile with new execution data
runtime/src/profile.rs:57
↓ 10 callersMethodis_empty
(&self)
runtime/src/mailbox.rs:99
↓ 10 callersMethodis_eof
Check if at end of file
leanr-syntax/src/lexer.rs:432
↓ 10 callersMethodpush_var
Push a simple variable binding
lean-agentic/src/context.rs:65
↓ 10 callersMethodsendRequest
* Send a JSON-RPC request
npm/lean-agentic/mcp/test-client.js:57
↓ 10 callersMethodsynth
Synthesis mode: infer the type of an expression Returns (term, type)
leanr-elab/src/elaborate.rs:156
↓ 10 callersMethodwait
* Wait for specified milliseconds
npm/lean-agentic/mcp/test-client.js:173
↓ 9 callersMethodcurrent
Get current token
leanr-syntax/src/parser.rs:687
↓ 9 callersMethodget
(&self, id: &str)
src/agentdb/episode_store.rs:24
↓ 9 callersMethodmk_pi
Create a Pi term
lean-agentic/src/arena.rs:145
↓ 9 callersFunctiontest
(name, fn)
npm/lean-agentic/tests/theorems/dependent-types.test.js:23
↓ 8 callersMethodadd_robot
Add a robot
examples/grid-operator/safety_bounded_grid.rs:157
↓ 8 callersMethodclose
* Close database connection
npm/lean-agentic/src/agentdb-integration.js:360
↓ 8 callersMethodcreateIdentity
()
npm/lean-agentic/src/web.js:41
↓ 8 callersFunctioncreate_test_robot
(id: &str)
examples/grid-operator/safety_bounded_grid.rs:359
↓ 8 callersMethodget
Get a level by its ID
lean-agentic/src/level.rs:111
↓ 8 callersMethodlen
Get the number of interned symbols
lean-agentic/src/symbol.rs:107
↓ 8 callersMethodprove_confluence
( &mut self, source: &str, target1: &str, target2: &str, )
leanr-theorems/src/wasm.rs:30
↓ 8 callersMethodpush
Push a new binding onto the context
lean-agentic/src/context.rs:60
↓ 8 callersFunctiontest
(name, fn)
npm/lean-agentic/tests/theorems/performance-theorems.test.js:23
↓ 8 callersMethodwhnf
Normalize a term to WHNF
leanr-eval-lite/src/normalize.rs:42
↓ 7 callersMethodadd_agent
Add agent to topology
runtime/src/topology.rs:40
↓ 7 callersMethodcheck
Checking mode: check that an expression has a given type
leanr-elab/src/elaborate.rs:425
↓ 7 callersMethodconstant
Create a concrete level
lean-agentic/src/level.rs:121
↓ 7 callersFunctioncreate_test_envelope
()
examples/grid-operator/safety_bounded_grid.rs:337
↓ 7 callersFunctioncreate_test_mandate
()
examples/trading/risk_bounded_trading.rs:385
↓ 7 callersMethodencode
(&self, graph: &LoopGraph)
src/llm-compiler/auto_vectorization.rs:154
↓ 7 callersMethodfresh
Create a fresh metavariable
leanr-elab/src/metavar.rs:42
↓ 7 callersMethodintern
Intern a level and return its ID
lean-agentic/src/level.rs:99
↓ 7 callersMethodis_def_eq
Check if two terms are definitionally equal
lean-agentic/src/conversion.rs:68
↓ 7 callersMethodparse_params
Parse function parameters
leanr-syntax/src/parser.rs:275
↓ 7 callersMethodsendResponse
* Send JSON-RPC response
npm/lean-agentic/mcp/server.js:272
↓ 6 callersMethodadd_zone
Add a safety zone
examples/grid-operator/safety_bounded_grid.rs:152
↓ 6 callersFunctioncreate_test_zone
(id: &str, has_human: bool)
examples/grid-operator/safety_bounded_grid.rs:347
↓ 6 callersMethodexecute
Execute financial action with proofs
examples/finance/verified_finance_agent.rs:226
↓ 6 callersMethodexecute_command
Execute control command with safety verification
examples/grid-operator/safety_bounded_grid.rs:234
↓ 6 callersMethodfresh_mvar
Create a fresh metavariable
leanr-elab/src/elaborate.rs:557
↓ 6 callersMethodfrom
(iso: Tracked<T, Iso>)
runtime/src/capabilities.rs:136
↓ 6 callersMethodget
(&self)
runtime/src/capabilities.rs:95
↓ 6 callersFunctiongetStringFromWasm0
(ptr, len)
npm/lean-agentic/wasm-web/leanr_wasm.js:28
↓ 6 callersFunctiongetStringFromWasm0
(ptr, len)
npm/lean-agentic/wasm-node/leanr_wasm.js:22
↓ 6 callersFunctiongetStringFromWasm0
(ptr, len)
examples/wasm-demo/leanr_wasm.js:28
↓ 6 callersMethodhash
Get the term's hash
lean-agentic/src/term.rs:161
↓ 6 callersMethodis_eof
Check if at end of input
leanr-syntax/src/parser.rs:701
↓ 6 callersMethodpayload
(&self)
runtime/src/message.rs:37
↓ 6 callersMethodpop
Pop the most recent binding for a name
leanr-elab/src/context.rs:51
↓ 6 callersMethodrecall
Recall episodes with explanation
examples/memory-copilot/explainable_memory.rs:184
↓ 6 callersMethodreduce
(&mut self, term: &str)
leanr-theorems/src/wasm.rs:88
↓ 6 callersMethodrun
Run the task
runtime/src/scheduler.rs:56
↓ 6 callersMethodsendError
* Send JSON-RPC error
npm/lean-agentic/mcp/server.js:284
↓ 6 callersMethodunify
Unify two terms
lean-agentic/src/unification.rs:95
↓ 6 callersMethodverify_signature
Verify Ed25519 signature
examples/ed25519_proof_signing.rs:146
next →1–100 of 1,015, ranked by callers