mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 16:21:46 +03:00
a44c8ddd5a
unelabBinder was losing information for the purpose of displaying names nicely. This is typically wanted but when working with elabortation it's useful to have all the information you can get. Things like record field names would be lost when querying with GetType but are now retained.
28 lines
1.2 KiB
Plaintext
28 lines
1.2 KiB
Plaintext
1/1: Building refprims (refprims.idr)
|
|
LOG 0: Name: Prelude.List.++
|
|
LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just xs) (Prelude.List a) (%pi RigW Explicit (Just {arg:6371}) (Prelude.List a) (Prelude.List a))))
|
|
LOG 0: Name: Prelude.Strings.++
|
|
LOG 0: Type: (%pi Rig1 Explicit (Just x) String (%pi Rig1 Explicit (Just y) String String))
|
|
LOG 0: Resolved name: Prelude.Nat
|
|
LOG 0: Constructors: [Prelude.Z, Prelude.S]
|
|
refprims.idr:43:10--43:27:While processing right hand side of dummy1 at refprims.idr:43:1--45:1:
|
|
Error during reflection: Not really trying at:
|
|
43 dummy1 = %runElab logPrims
|
|
^^^^^^^^^^^^^^^^^
|
|
|
|
refprims.idr:46:10--46:30:While processing right hand side of dummy2 at refprims.idr:46:1--48:1:
|
|
Error during reflection: Still not trying at:
|
|
46 dummy2 = %runElab logDataCons
|
|
^^^^^^^^^^^^^^^^^^^^
|
|
|
|
refprims.idr:49:10--49:25:While processing right hand side of dummy3 at refprims.idr:49:1--51:1:
|
|
Error during reflection: Undefined name at:
|
|
49 dummy3 = %runElab logBad
|
|
^^^^^^^^^^^^^^^
|
|
|
|
refprims.idr:52:10--52:28:While processing right hand side of dummy4 at refprims.idr:52:1--54:1:
|
|
Error during reflection: failed after generating Main.{plus:XXXX} at:
|
|
52 dummy4 = %runElab tryGenSym
|
|
^^^^^^^^^^^^^^^^^^
|
|
|