idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-23 19:54:50 +03:00
Code Issues Projects Releases Wiki Activity
6b768f28b1
Idris2/tests/idris2/basic044/expected

169 lines
9.6 KiB
Plaintext
Raw Normal View History

[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
1/1: Building Term (Term.idr)
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.type:1: Processing Term.Typ
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.data:1: Processing Term.Bdr
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG unify.equal:10: Skipped unification (equal already): Type and Type
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.data:1: Processing Term.Chk
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:n:N}, (Term:L:C--L:C, Rig0))
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.data:1: Processing Term.Syn
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0))
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.def.lhs:3: LHS term: Term.Typ
[ fix ] Remove stray ")" in Show instance for Term (#2611)
2022-08-08 17:24:07 +03:00
LOG unify.equal:10: Skipped unification (equal already): (vars : $resolvedN) -> Type and (vars : $resolvedN) -> Type
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG declare.def.clause:3: RHS term: Term.Chk
LOG declare.def:2: Case tree for Term.Typ: [0] Term.Chk
LOG declare.def:3: Working from [0] Term.Chk
[ test ] cleanup basic044 All of these internal names are making the output fragile. This cleanup should allow us to only have to update the golden file when there is a genuinely interesting change.
2020-08-25 10:51:58 +03:00
LOG declare.def:3: Catch all case in N
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG declare.def:3: Initially missing in Term.Typ:
LOG declare.type:1: Processing Term.Term
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.def.lhs:3: LHS term: Term.Term
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.def.clause:3: RHS term: (Term.Chk Prelude.Basics.True)
LOG declare.def:2: Case tree for Term.Term: [0] (Term.Chk Prelude.Basics.True)
LOG declare.def:3: Working from [0] (Term.Chk Prelude.Basics.True)
[ test ] cleanup basic044 All of these internal names are making the output fragile. This cleanup should allow us to only have to update the golden file when there is a genuinely interesting change.
2020-08-25 10:51:58 +03:00
LOG declare.def:3: Catch all case in N
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG declare.def:3: Initially missing in Term.Term:
LOG declare.type:1: Processing Term.NF
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.def.lhs:3: LHS term: Term.NF
LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.def.clause:3: RHS term: (Term.Chk Prelude.Basics.False)
LOG declare.def:2: Case tree for Term.NF: [0] (Term.Chk Prelude.Basics.False)
LOG declare.def:3: Working from [0] (Term.Chk Prelude.Basics.False)
[ test ] cleanup basic044 All of these internal names are making the output fragile. This cleanup should allow us to only have to update the golden file when there is a genuinely interesting change.
2020-08-25 10:51:58 +03:00
LOG declare.def:3: Catch all case in N
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG declare.def:3: Initially missing in Term.NF:
Term> Bye for now!
1/1: Building Vec (Vec.idr)
LOG declare.type:1: Processing Vec.Vec
[ fix ] Remove stray ")" in Show instance for Term (#2611)
2022-08-08 17:24:07 +03:00
LOG declare.def:2: Case tree for Vec.Vec: [0] ({arg:N} : (Data.Fin.Fin {arg:N}[1])) -> {arg:N}[1]
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG declare.type:1: Processing Vec.Nil
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] (Data.Fin.Fin Prelude.Types.Z) Data.Fin.Uninhabited implementation at Data.Fin:L:C--L:C)
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG declare.type:1: Processing Vec.::
[ debug ] pretty printer for case trees (#652)
2020-09-09 18:22:22 +03:00
LOG declare.def:2: Case tree for Vec.::: case {arg:N}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:N}[0])) of
{ Data.Fin.FZ {e:N} => [0] {arg:N}[3]
| Data.Fin.FS {e:N} {e:N} => [1] ({arg:N}[5] {e:N}[1])
}
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
LOG declare.type:1: Processing Vec.test
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
[ refactor ] Index Pretty over the type of annotations (#2371)
2022-04-27 14:26:59 +03:00
($resolvedN 2)
($resolvedN 2)
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
With default. Target type : Prelude.Types.Nat
Add symmetric and transitive closure relations
2023-05-05 15:34:48 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration (kept 4 out of 4 candidates) (not delayed) at Vec:L:C--L:C:
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
[ log ] more readable output for elab.ambiguous (#1500)
2021-06-03 20:19:08 +03:00
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
[ fix ] Remove stray ")" in Show instance for Term (#2611)
2022-08-08 17:24:07 +03:00
Target type : ({arg:N} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) -> (Prelude.Basics.List Prelude.Types.Nat)
Add symmetric and transitive closure relations
2023-05-05 15:34:48 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
$resolvedN
[ log ] more readable output for elab.ambiguous (#1500)
2021-06-03 20:19:08 +03:00
$resolvedN
$resolvedN
[ test ] cleanup basic044 All of these internal names are making the output fragile. This cleanup should allow us to only have to update the golden file when there is a genuinely interesting change.
2020-08-25 10:51:58 +03:00
Target type : ?Vec.{a:N}_[]
Add symmetric and transitive closure relations
2023-05-05 15:34:48 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration (kept 4 out of 4 candidates) (not delayed) at Vec:L:C--L:C:
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
[ log ] more readable output for elab.ambiguous (#1500)
2021-06-03 20:19:08 +03:00
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
Use Closures instead of NF in binders for normal forms (#1823) * Skip forced arguments in conversion check This isn't always safe - we have to have also checked the type of the things we're converting - but in the place where it is safe it can be a pretty significant saving. * Use Closures, not NF, in Binders for normal forms This means we don't need to reduce argument types during unification if we don't need to. Also, we now try to avoid reducing closures during unification if they are unified with a metavariable. Together, this saves a huge amount of unnecessary evaluation in programs that do a lot of compile time evaluation. * Didn't mean to update idris2api.ipkg * Fix dodgy merge
2021-08-08 19:05:29 +03:00
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
Add symmetric and transitive closure relations
2023-05-05 15:34:48 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration (kept 4 out of 4 candidates) (not delayed) at Vec:L:C--L:C:
(($resolvedN (fromInteger 0)) Nil)
[ log ] more readable output for elab.ambiguous (#1500)
2021-06-03 20:19:08 +03:00
(($resolvedN (fromInteger 0)) Nil)
(($resolvedN (fromInteger 0)) Nil)
(($resolvedN (fromInteger 0)) Nil)
[ test ] cleanup basic044 All of these internal names are making the output fragile. This cleanup should allow us to only have to update the golden file when there is a genuinely interesting change.
2020-08-25 10:51:58 +03:00
Target type : ?Vec.{a:N}_[]
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
[ refactor ] Index Pretty over the type of annotations (#2371)
2022-04-27 14:26:59 +03:00
($resolvedN 0)
($resolvedN 0)
[ test ] cleanup basic044 All of these internal names are making the output fragile. This cleanup should allow us to only have to update the golden file when there is a genuinely interesting change.
2020-08-25 10:51:58 +03:00
With default. Target type : ?Vec.{a:N}_[]
Add symmetric and transitive closure relations
2023-05-05 15:34:48 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
$resolvedN
[ log ] more readable output for elab.ambiguous (#1500)
2021-06-03 20:19:08 +03:00
$resolvedN
$resolvedN
Use Closures instead of NF in binders for normal forms (#1823) * Skip forced arguments in conversion check This isn't always safe - we have to have also checked the type of the things we're converting - but in the place where it is safe it can be a pretty significant saving. * Use Closures, not NF, in Binders for normal forms This means we don't need to reduce argument types during unification if we don't need to. Also, we now try to avoid reducing closures during unification if they are unified with a metavariable. Together, this saves a huge amount of unnecessary evaluation in programs that do a lot of compile time evaluation. * Didn't mean to update idris2api.ipkg * Fix dodgy merge
2021-08-08 19:05:29 +03:00
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
Add symmetric and transitive closure relations
2023-05-05 15:34:48 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
($resolvedN 0)
($resolvedN 0)
With default. Target type : (?Vec.{rel:N}_[] ?Vec.{x:N}_[] ?Vec.{y:N}_[])
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
[ refactor ] Index Pretty over the type of annotations (#2371)
2022-04-27 14:26:59 +03:00
($resolvedN 0)
($resolvedN 0)
[ test ] cleanup basic044 All of these internal names are making the output fragile. This cleanup should allow us to only have to update the golden file when there is a genuinely interesting change.
2020-08-25 10:51:58 +03:00
With default. Target type : ?Vec.{a:N}_[]
Add symmetric and transitive closure relations
2023-05-05 15:34:48 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
$resolvedN
[ log ] more readable output for elab.ambiguous (#1500)
2021-06-03 20:19:08 +03:00
$resolvedN
$resolvedN
Use Closures instead of NF in binders for normal forms (#1823) * Skip forced arguments in conversion check This isn't always safe - we have to have also checked the type of the things we're converting - but in the place where it is safe it can be a pretty significant saving. * Use Closures, not NF, in Binders for normal forms This means we don't need to reduce argument types during unification if we don't need to. Also, we now try to avoid reducing closures during unification if they are unified with a metavariable. Together, this saves a huge amount of unnecessary evaluation in programs that do a lot of compile time evaluation. * Didn't mean to update idris2api.ipkg * Fix dodgy merge
2021-08-08 19:05:29 +03:00
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
Add symmetric and transitive closure relations
2023-05-05 15:34:48 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 4 candidates) (delayed) at Vec:L:C--L:C:
[ log ] more readable output for elab.ambiguous (#1500)
2021-06-03 20:19:08 +03:00
(($resolvedN (fromInteger 0)) Nil)
[ breaking ] making toList part of Foldable (#1395)
2021-05-11 10:26:00 +03:00
Target type : (Prelude.Basics.List Prelude.Types.Nat)
[ new ] `--install-with-src`; refactoring around `FC`s (#1450) Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
2021-06-05 14:53:22 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
[ refactor ] Index Pretty over the type of annotations (#2371)
2022-04-27 14:26:59 +03:00
($resolvedN 0)
($resolvedN 0)
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
With default. Target type : Prelude.Types.Nat
Add symmetric and transitive closure relations
2023-05-05 15:34:48 +03:00
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:L:C--L:C:
[ log ] more readable output for elab.ambiguous (#1500)
2021-06-03 20:19:08 +03:00
$resolvedN
[ breaking ] making toList part of Foldable (#1395)
2021-05-11 10:26:00 +03:00
Target type : (Prelude.Basics.List Prelude.Types.Nat)
Inline small metavariables Where 'small' means they don't refer to other metavariables, except right at the top level, and they don't go beyond a certain small depth, arrived at by experimenting. We already did a bit of this, but only for depth 0. The effect of this is that we don't need to save out lots of metavariables, so ttc loading is faster. This takes about 8s off the Idris build time!
2021-05-18 19:56:36 +03:00
LOG declare.def:2: Case tree for Vec.test: [0] (Vec.:: (Prelude.Types.S Prelude.Types.Z) (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.:: Prelude.Types.Z (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.:: Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil (Prelude.Basics.List Prelude.Types.Nat))))
[ new ] topics for logging levels (#569)
2020-08-20 20:45:34 +03:00
Vec> Bye for now!
Reference in New Issue Copy Permalink