| 1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253 |
- It should be possible to refer to implicit arguments by name, to avoid having
- long sequences of {_}.
- Given
- f : {...}{A:Set} -> ...
- you should be able to say
- f {A = Nat}
- to give A explicitly. This should also work in patterns:
- f {A = A} = .. A ..
- How will this work exactly?
- At the moment we have the judgement form (checkArgs)
- Γ ⊢ es fits A ↓ vs
- with rules
- Γ ⊢ e ↑ A ─→ v Γ ⊢ es fits B[v/x]
- ----------------------------------
- Γ ⊢ e es fits (x:A)B ─→ v vs
- Γ ⊢ e es fits B[α/x]
- ----------------------------
- Γ ⊢ e es fits {x:A}B ─→ α vs
- Γ ⊢ e ↑ A ─→ v Γ ⊢ es fits B[v/x]
- ----------------------------------
- Γ ⊢ {e}es fits {x:A}B ─→ α vs
- Γ ⊢ ∙ fits B[α/x] ─→ vs
- -----------------------------
- Γ ⊢ ∙ fits {x:A} -> B ─→ α vs
- To this we add the rules
- Γ ⊢ e ↑ A ─→ v Γ ⊢ es fits B[v/x]
- ---------------------------------- (same as the {e}es rule)
- Γ ⊢ {x=e}es fits {x:A}B
- Γ ⊢ {x=e}es fits B[α/y] ─→ vs
- ------------------------------- (x ≠ y, similar to the 'e es fits {x:A}B' rule)
- Γ ⊢ {x=e}es fits {y:A}B ─→ α vs
- What about patterns? It would work exactly the same. I.e two new rules very
- similar to the '{p}ps' and 'p ps : {x:A}B' rules.
|
