{"_id":"@cooljapan/oxilean","_rev":"4-b57c8fc9abfaa44793cb73d86b77d5c4","name":"@cooljapan/oxilean","dist-tags":{"latest":"0.1.3"},"versions":{"0.1.0":{"name":"@cooljapan/oxilean","version":"0.1.0","keywords":["lean","lean4","proof-assistant","type-theory","wasm","webassembly","theorem-prover"],"author":{"url":"Team Kitasan","name":"COOLJAPAN OU"},"license":"Apache-2.0","_id":"@cooljapan/oxilean@0.1.0","maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"homepage":"https://github.com/cool-japan/oxilean","bugs":{"url":"https://github.com/cool-japan/oxilean/issues"},"dist":{"shasum":"89064de40c538b27b72b46957ad7c2fc3d90af91","tarball":"https://registry.npmjs.org/@cooljapan/oxilean/-/oxilean-0.1.0.tgz","fileCount":6,"integrity":"sha512-Yvq7qDo6hdfNCaj53bIo7KzIfjAHC9iuIfUo75YJrMBv+9ee87FcFZ0c1e0XOtYoa/eH4JW4Cg6eRZgK1hW2jQ==","signatures":[{"sig":"MEUCIGBhMcV6Z9Ihe/FbV+VTedP7AxySVPwPP3j1IH3IFzktAiEAs0LKjC2RUnC1VLiEyoyMvZHMV3/ysA6FukZKi3bLFzk=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":60981},"main":"oxilean_wasm.js","type":"module","types":"oxilean_wasm.d.ts","gitHead":"e6e04455b283e81bbe9be18ecb8f55b846e63c13","_npmUser":{"name":"kitasan","email":"info@kitasan.io"},"repository":{"url":"git+https://github.com/cool-japan/oxilean.git","type":"git"},"_npmVersion":"11.2.0","description":"OxiLean - Lean4-compatible proof assistant for JavaScript/TypeScript","directories":{},"sideEffects":["./oxilean_wasm.js","./snippets/*"],"_nodeVersion":"23.7.0","collaborators":["COOLJAPAN OU (Team Kitasan)"],"_hasShrinkwrap":false,"_npmOperationalInternal":{"tmp":"tmp/oxilean_0.1.0_1772671960897_0.0879029173171404","host":"s3://npm-registry-packages-npm-production"}},"0.1.1":{"name":"@cooljapan/oxilean","version":"0.1.1","keywords":["lean","wasm","webassembly","type-theory","browser"],"license":"Apache-2.0","_id":"@cooljapan/oxilean@0.1.1","maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"homepage":"https://github.com/cool-japan/oxilean","bugs":{"url":"https://github.com/cool-japan/oxilean/issues"},"dist":{"shasum":"e8f040f72362398a873179f01f03f1c41d1b2ad2","tarball":"https://registry.npmjs.org/@cooljapan/oxilean/-/oxilean-0.1.1.tgz","fileCount":5,"integrity":"sha512-WR2RzpxsfWIKO5dZ/wpdMOYqmYC1eReUwIImJmb8e5JJ0ElZs0Sx+9c7JfKVVTmzLoHcbecMcSs7vHpZs/xelw==","signatures":[{"sig":"MEUCIQDIWs62Eqo0rtjasAovlcDW5IexvceIZcAGx5+m9cke/gIgSYURGTH2jZIxo2EuSIRi8axp6sv3UW4Snq6R0X13+lA=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":66123},"main":"oxilean_wasm.js","type":"module","types":"oxilean_wasm.d.ts","gitHead":"c85fe9f0dd21b03d6c9c617ef5cf088dfabf2712","_npmUser":{"name":"kitasan","email":"info@kitasan.io"},"repository":{"url":"git+https://github.com/cool-japan/oxilean.git","type":"git"},"_npmVersion":"11.2.0","description":"OxiLean - Lean4-compatible proof assistant for JavaScript/TypeScript","directories":{},"sideEffects":["./snippets/*"],"_nodeVersion":"23.7.0","collaborators":["COOLJAPAN OU (Team Kitasan)"],"_hasShrinkwrap":false,"_npmOperationalInternal":{"tmp":"tmp/oxilean_0.1.1_1773038032607_0.5108853857233837","host":"s3://npm-registry-packages-npm-production"}},"0.1.2":{"name":"@cooljapan/oxilean","version":"0.1.2","keywords":["lean","wasm","webassembly","type-theory","browser"],"license":"Apache-2.0","_id":"@cooljapan/oxilean@0.1.2","maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"homepage":"https://github.com/cool-japan/oxilean","bugs":{"url":"https://github.com/cool-japan/oxilean/issues"},"dist":{"shasum":"38d228d31096ee9854d295c2cbad27f6b82d599e","tarball":"https://registry.npmjs.org/@cooljapan/oxilean/-/oxilean-0.1.2.tgz","fileCount":6,"integrity":"sha512-evumD9kdWavVVhYiNqoFIWdzqfdKYJcd3q4013W+19BCQZeUU2OTOOOOzMwZmwUXjliSSq/4nVW2NGQJ8IrwPA==","signatures":[{"sig":"MEQCIBDdZpD+b1KhrFx/AT6kcoziMwOxmQ+y6blYLuWguZx/AiAxOYc6pxagkSYzADpETDPsRLhd+I8BxwaqAjaOQjfliA==","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":21358},"main":"oxilean_wasm.js","type":"module","types":"oxilean_wasm.d.ts","_npmUser":{"name":"kitasan","email":"info@kitasan.io"},"repository":{"url":"git+https://github.com/cool-japan/oxilean.git","type":"git"},"_npmVersion":"10.9.7","description":"WebAssembly bindings for OxiLean","directories":{},"sideEffects":["./oxilean_wasm.js","./snippets/*"],"_nodeVersion":"22.22.2","collaborators":["COOLJAPAN OU (Team Kitasan)"],"_hasShrinkwrap":false,"_npmOperationalInternal":{"tmp":"tmp/oxilean_0.1.2_1777817092395_0.17945721982255214","host":"s3://npm-registry-packages-npm-production"}},"0.1.3":{"name":"@cooljapan/oxilean","type":"module","collaborators":["COOLJAPAN OU (Team Kitasan)"],"description":"WebAssembly bindings for OxiLean","version":"0.1.3","license":"Apache-2.0","repository":{"type":"git","url":"git+https://github.com/cool-japan/oxilean.git"},"main":"oxilean_wasm.js","homepage":"https://github.com/cool-japan/oxilean","types":"oxilean_wasm.d.ts","sideEffects":["./oxilean_wasm.js","./snippets/*"],"keywords":["lean","wasm","webassembly","type-theory","browser"],"_id":"@cooljapan/oxilean@0.1.3","bugs":{"url":"https://github.com/cool-japan/oxilean/issues"},"_nodeVersion":"22.23.1","_npmVersion":"10.9.8","dist":{"integrity":"sha512-dHiNq2o208A+0rjLVeYLZICXpsr/ON1n2gZaIcyobB79u+14a6mqrE4a4pPNnlnS+GbAdejvMWmX6pDvGlGoCQ==","shasum":"6cfe411e4b6e08617339853f6016a50e42dfacb2","tarball":"https://registry.npmjs.org/@cooljapan/oxilean/-/oxilean-0.1.3.tgz","fileCount":6,"unpackedSize":2004943,"signatures":[{"keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U","sig":"MEUCIQCYLr0Dy/PkHKgusX3EuKF3x8Rj1ZCLVlyy7KWQnMQEpAIgIliq7d/I9mF+eY+ZLQFg/4PgAavduSWaN7gd5tfxu2M="}]},"_npmUser":{"name":"kitasan","email":"info@kitasan.io"},"directories":{},"maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"_npmOperationalInternal":{"host":"s3://npm-registry-packages-npm-production","tmp":"tmp/oxilean_0.1.3_1784225683172_0.5144627101544847"},"_hasShrinkwrap":false}},"time":{"created":"2026-03-05T00:52:40.798Z","modified":"2026-07-16T18:14:43.658Z","0.1.0":"2026-03-05T00:52:41.065Z","0.1.1":"2026-03-09T06:33:52.774Z","0.1.2":"2026-05-03T14:04:52.546Z","0.1.3":"2026-07-16T18:14:43.477Z"},"bugs":{"url":"https://github.com/cool-japan/oxilean/issues"},"license":"Apache-2.0","homepage":"https://github.com/cool-japan/oxilean","keywords":["lean","wasm","webassembly","type-theory","browser"],"repository":{"type":"git","url":"git+https://github.com/cool-japan/oxilean.git"},"description":"WebAssembly bindings for OxiLean","maintainers":[{"name":"kitasan","email":"info@kitasan.io"}],"readme":"# oxilean-wasm\n\n[![Crates.io](https://img.shields.io/crates/v/oxilean-wasm.svg)](https://crates.io/crates/oxilean-wasm)\n[![Docs.rs](https://docs.rs/oxilean-wasm/badge.svg)](https://docs.rs/oxilean-wasm)\n[![npm](https://img.shields.io/npm/v/@cooljapan/oxilean)](https://www.npmjs.com/package/@cooljapan/oxilean)\n\n> **WebAssembly Bindings for the OxiLean Theorem Prover**\n\n`oxilean-wasm` exposes the OxiLean type checker and proof engine as a WebAssembly module that can be loaded directly in web browsers or Node.js environments. It provides a JavaScript/TypeScript-friendly API so that web applications, online proof assistants, and editor extensions can drive OxiLean without any server-side infrastructure.\n\nThe npm package is published as [`@cooljapan/oxilean`](https://www.npmjs.com/package/@cooljapan/oxilean).\n\n59 tests passing -- full integration with the kernel/parse/elab pipeline.\n\nPart of the [OxiLean](https://github.com/cool-japan/oxilean) project -- a Lean-compatible theorem prover implemented in pure Rust.\n\n## Install\n\n```bash\nnpm install @cooljapan/oxilean\n```\n\n## Modules\n\n| Module | Description |\n|--------|-------------|\n| `api` | Core OxiLean API (platform-independent logic) |\n| `types` | Value types, result structs, and conversion helpers |\n| `error` | WASM-compatible error type |\n| `wasm_api` | `#[wasm_bindgen]` entry points for JavaScript *(requires `wasm` feature)* |\n\n## Feature Flags\n\n| Feature | Enables |\n|---------|---------|\n| `wasm` | `wasm-bindgen`, `serde`, `serde_json`, `serde-wasm-bindgen`, `js-sys` |\n\n## API\n\nThe `wasm_api` module exports the `WasmOxiLean` class and convenience functions:\n\n```typescript\nimport { WasmOxiLean, checkSource, getVersion } from '@cooljapan/oxilean';\n\nconst ox = new WasmOxiLean();\n\n// Check source code\nconst result = ox.check('theorem foo : True := trivial');\n// result: { success: boolean, declarations: DeclInfo[], errors: ErrorInfo[], warnings: WarningInfo[] }\n\n// REPL\nconst repl = ox.repl('#check Nat');\n// repl: { output: string, goals: GoalInfo[], success: boolean, error?: string }\n\n// Completions at a position\nconst completions = ox.completions(source, line, col);\n// completions: CompletionItem[]\n\n// Hover info at a position\nconst hover = ox.hoverInfo(source, line, col); // string | null\n\n// Format source code\nconst formatted = ox.format(source); // string\n\n// Properties\nox.sessionId;       // getter -- unique session identifier\nox.history();       // string[] -- REPL command history\nox.clearHistory();  // clear REPL history\nWasmOxiLean.version(); // static -- OxiLean version string\n\n// Convenience functions (no instance needed)\ncheckSource('theorem foo : True := trivial');\ngetVersion();\n\n// Clean up WASM memory when done\nox.free();\n```\n\n## Building\n\nThe build script produces three targets: bundler (webpack/vite), web (browser direct), and nodejs.\n\n```bash\n# From the crate directory\nbash build-wasm.sh\n```\n\nThis creates:\n\n- `pkg/` -- bundler target (primary)\n- `pkg-web/` -- web target\n- `pkg-nodejs/` -- nodejs target\n\n## Dependencies\n\nAll dependencies are optional and gated behind the `wasm` feature:\n\n- `wasm-bindgen` 0.2.114\n- `serde` + `serde_json`\n- `serde-wasm-bindgen` 0.6.5\n- `js-sys` 0.3.83\n\n## Testing\n\n```bash\n# Unit tests (native target)\ncargo test -p oxilean-wasm\n\n# WASM tests in headless browser (requires wasm-pack)\nwasm-pack test crates/oxilean-wasm --headless --chrome\n```\n\n## License\n\nCopyright COOLJAPAN OU (Team Kitasan). Apache-2.0 -- See [LICENSE](../../LICENSE) for details.\n","readmeFilename":"README.md"}