mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2025-01-02 01:32:54 +03:00
Allow annotating record fields with multiplicities
Default is still 1, so only 0 has any effect. (Might revisit this later, perhaps default should be omega?)
This commit is contained in:
parent
76af4518b1
commit
e0b3839792
@ -1137,12 +1137,17 @@ fieldDecl fname indents
|
||||
fieldBody : PiInfo -> Rule (List PField)
|
||||
fieldBody p
|
||||
= do start <- location
|
||||
m <- multiplicity
|
||||
rigin <- getMult m
|
||||
let rig = case rigin of
|
||||
Rig0 => Rig0
|
||||
_ => Rig1
|
||||
ns <- sepBy1 (symbol ",") unqualifiedName
|
||||
symbol ":"
|
||||
ty <- expr pdef fname indents
|
||||
end <- location
|
||||
pure (map (\n => MkField (MkFC fname start end)
|
||||
Rig1 p (UN n) ty) ns)
|
||||
rig p (UN n) ty) ns)
|
||||
|
||||
recordDecl : FileName -> IndentInfo -> Rule PDecl
|
||||
recordDecl fname indents
|
||||
|
Loading…
Reference in New Issue
Block a user