[ new ] allow auto fields in records

src/Idris/Parser.idr

@@ -1251,7 +1251,8 @@ fieldDecl fname indents
       = do doc <- option "" documentation
            symbol "{"
            commit
-           fs <- fieldBody doc Implicit
+           impl <- option Implicit (AutoImplicit <$ keyword "auto")
+           fs <- fieldBody doc impl
            symbol "}"
            atEnd indents
            pure fs

tests/Main.idr

@@ -95,6 +95,7 @@ idrisTests
        "real001", "real002",
        -- Records, access and dependent update
        "record001", "record002", "record003", "record004", "record005",
+       "record007",
        -- Quotation and reflection
        "reflection001", "reflection002", "reflection003", "reflection004",
        "reflection005", "reflection006", "reflection007", "reflection008",

tests/idris2/record007/Fld.idr

@@ -0,0 +1,6 @@
+record Is3 (n : Nat) where
+  constructor MkThree
+  {auto prf : n === 3}
+
+three : Is3 3
+three = MkThree

tests/idris2/record007/expected

@@ -0,0 +1,3 @@
+1/1: Building Fld (Fld.idr)
+Main> Main> MkThree {n = 3} {prf = Refl {a = Nat} {x = 3}}
+Main> Bye for now!

tests/idris2/record007/input

@@ -0,0 +1,3 @@
+:set showimplicits
+three
+:q

tests/idris2/record007/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner Fld.idr < input
+
+rm -rf build