|
| 1 | +# SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +# |
| 3 | +# Idris 2 + base / contrib library synonyms. |
| 4 | +# Schema: see data/synonyms/README.adoc. |
| 5 | +# Seeded 2026-04-28 alongside the cross-prover semantic-class |
| 6 | +# extension (Step 2 of the N-dim VeriSim corpus plan). |
| 7 | + |
| 8 | +# --------------------------------------------------------------------------- |
| 9 | +# Well-foundedness (cross-prover semantic class) |
| 10 | +# --------------------------------------------------------------------------- |
| 11 | + |
| 12 | +[[synonym]] |
| 13 | +canonical = "WellFounded" |
| 14 | +aliases = ["WellFounded R", "Wf"] |
| 15 | +tactic_class = "wf-statement" |
| 16 | +semantic_class = "well-foundedness" |
| 17 | +notes = """ |
| 18 | +`WellFounded R` in `Control.WellFounded` (base): every R-chain is |
| 19 | +finite. Same conceptual role as Agda's `WellFounded`, Coq's |
| 20 | +`well_founded`, and Lean 4's `WellFounded`. |
| 21 | +""" |
| 22 | + |
| 23 | +[[synonym]] |
| 24 | +canonical = "Accessible" |
| 25 | +aliases = ["Acc", "Acc R x"] |
| 26 | +tactic_class = "wf-witness" |
| 27 | +semantic_class = "accessibility" |
| 28 | +notes = """ |
| 29 | +`Accessible R x` in `Control.WellFounded`. Idris 2's name differs |
| 30 | +from the others; the type-shape is identical. |
| 31 | +""" |
| 32 | + |
| 33 | +[[synonym]] |
| 34 | +canonical = "wfRec" |
| 35 | +aliases = ["WellFounded.induction", "well-founded-induction"] |
| 36 | +tactic_class = "wf-recursor" |
| 37 | +semantic_class = "wf-induction" |
| 38 | +notes = """ |
| 39 | +Well-founded recursion derived from `WellFounded`. |
| 40 | +""" |
| 41 | + |
| 42 | +# --------------------------------------------------------------------------- |
| 43 | +# Banned / dangerous patterns |
| 44 | +# --------------------------------------------------------------------------- |
| 45 | + |
| 46 | +[[synonym]] |
| 47 | +canonical = "believe_me" |
| 48 | +aliases = ["unsafeCoerce", "Obj.magic"] |
| 49 | +tactic_class = "danger" |
| 50 | +notes = """ |
| 51 | +Idris 2's unsafe cast. BANNED across the whole hyperpolymath estate |
| 52 | +(panic-attack rejects). Use a constructive proof or a `partial` |
| 53 | +totality annotation instead. |
| 54 | +""" |
| 55 | + |
| 56 | +[[synonym]] |
| 57 | +canonical = "assert_total" |
| 58 | +aliases = ["assert_smaller", "%total-fudge"] |
| 59 | +tactic_class = "danger" |
| 60 | +notes = """ |
| 61 | +Tells the totality checker to trust this call without proof. Avoid; |
| 62 | +restructure to a structurally-decreasing recursion or use |
| 63 | +`well-founded-recursion` with an explicit measure. |
| 64 | +""" |
| 65 | + |
| 66 | +[[synonym]] |
| 67 | +canonical = "idris_crash" |
| 68 | +aliases = ["partial-stub"] |
| 69 | +tactic_class = "stub" |
| 70 | +notes = """ |
| 71 | +Per project memory (Cerro-Torre 2026-04-25): `partial + idris_crash` |
| 72 | +is the accepted pattern for postulate-style stubs that downstream |
| 73 | +proofs are allowed to depend on, provided the dependent is also |
| 74 | +annotated `partial` and the design intent is documented. |
| 75 | +
|
| 76 | +Not preferred for new code, but recognised as the workaround when |
| 77 | +Idris 2 0.8.0's `postulate` is unavailable in the desired position. |
| 78 | +""" |
0 commit comments