Syntax highlighting — full syntax highlighting for .ae files
Diagnostics — type errors and parse errors shown inline as you type
Hover types — hover over any identifier to see its inferred type
Hole synthesis — place a ?holeName in your code, then use Refactor… (or the lightbulb) to synthesize a solution with your chosen synthesizer
Synthesizers
When synthesizing a hole the following backends are available via the Refactor code-action menu:
Identifier
Description
tdsyn_enumerative
Type-directed synthesis (breadth-first search with SMT-solved leaves)
tdsyn
Type-directed synthesis (alias for tdsyn_enumerative)
tactics
Random tactic search (Lean-style)
gp
Genetic programming (default)
enumerative
Exhaustive enumerative search
random_search
Random program search
synquid
Synquid-style type-directed enumerative synthesis
hc
Hill climbing
1p1
One-plus-one evolutionary strategy
smt
SMT-guided synthesis via z3 (best for arithmetic/boolean constraints)
decision_tree
Decision tree regressor fitted from @csv_data examples
llm
LLM-based synthesis via Ollama
You can set a preferred synthesizer via the aeon.defaultSynthesizer setting — it will appear first in the code-action list.
Requires AeonLang 4.5.1 or newer on PyPI (or a local checkout via aeon.localPackagePath). The extension invokes the compiler exclusively through uv / uvx — no system Python or managed venv is used.
Configuration
Setting
Default
Description
aeon.localPackagePath
""
Path to a local aeon source tree (uses uvx --from <path>)
aeon.defaultSynthesizer
"gp"
Preferred synthesizer shown first in the code-action menu
