IdrisPro will be a native macOS IDE for Idris 2, built on APIAnyware-MacOS bindings for native macOS APIs, with WebKit as a UI layer and Monaco as the code editor.

IdrisPro is currently in the design phase. No code has been written yet.

Why a Dedicated Idris IDE?

Idris 2 is a dependently-typed language where programming and proving are the same activity. Development is interactive and hole-driven — you write types first, leave holes where implementations should go, and let the type system guide you toward correct programs. IdrisPro provides purpose-built tooling for proof-driven development, dependent type exploration, and the kind of interactive elaboration that makes Idris productive.

Planned Features

• Interactive hole filling — view proof obligations for each hole, with type-directed suggestions
• Case splitting — automatically generate pattern-match cases from a type
• Proof search — automated search for terms that satisfy a given type
• Dependent type inspector — explore types that depend on values, visualize type families
• Totality checker integration — see which functions are total, partial, or covering
• Elaborator reflection tools — inspect and debug metaprograms
• Implicit argument visualization — see what the elaborator inferred for implicit arguments
• Native macOS integration via APIAnyware-MacOS bindings — no Tauri or Electron