edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-27 00:38:13 +03:00
Code Issues Projects Releases Wiki Activity

Commit Graph

  • 35994b81e9 Port prelude's inline API documentation from Idris 1 Kamil Shakirov 2020-04-22 01:40:40 +0600
  • 0e73bf976b Updated the CHANGELOG to mention literate mode. Jan de Muijnck-Hughes 2020-04-07 10:07:28 +0100
  • 89b68d7771 Added documentation on literate modes to the reference document. Jan de Muijnck-Hughes 2020-04-07 10:01:48 +0100
  • 203bc3cb66 Removed bird style hidden lines from style. Jan de Muijnck-Hughes 2020-04-07 10:01:21 +0100
  • af27bce2e2 Enhance literate mode to recognise multi-modes. Jan de Muijnck-Hughes 2020-03-31 23:22:15 +0100
  • be8b157ead
         Merge pull request #290 from LibreCybernetics/minor-unicode-identifier-fixes Edwin Brady 2020-04-21 18:09:58 +0100
  • 1a41a265b9
         Merge pull request #299 from chrrasmussen/fix-chez-in-folder-with-spaces Edwin Brady 2020-04-21 17:04:37 +0100
  • 6ea8b477ed Refactor ident to reuse in IDEMode, fixes out of sync bug. Fabián Heredia Montiel 2020-04-15 14:48:40 -0500
  • 2a3213d10a
         Merge branch 'master' into fix-chez-in-folder-with-spaces Christian Rasmussen 2020-04-21 15:01:01 +0200
  • 2b6000ecac Shuffle some tests around Edwin Brady 2020-04-21 12:03:49 +0100
  • 2ad1621a3e Regression test for using named implementations Edwin Brady 2020-04-21 11:51:44 +0100
  • d39c701f28 Add 'using' hints at the right time Edwin Brady 2020-04-21 11:44:52 +0100
  • 71cae356e2
         Merge pull request #281 from ziman/fix-cast-double-int Edwin Brady 2020-04-21 11:24:09 +0100
  • 627d2c2f2b
         Merge pull request #292 from ohad/fully-abstract-records Edwin Brady 2020-04-21 10:59:51 +0100
  • 9aca77c5dd
         Merge pull request #293 from gallais/casetree Edwin Brady 2020-04-21 10:54:12 +0100
  • 60c4f8e178
         Merge pull request #287 from Porges/patch-1 Edwin Brady 2020-04-21 10:52:00 +0100
  • afa90c6ddc
         Merge pull request #284 from abailly/integral-operations Edwin Brady 2020-04-21 10:51:18 +0100
  • 8a0063a016
         Merge pull request #280 from gallais/comments Edwin Brady 2020-04-21 10:49:24 +0100
  • 69e774bd00 Merge branch 'jeetu7-master' Edwin Brady 2020-04-21 10:48:11 +0100
  • 9930b64c1c Merge branch 'master' of https://github.com/jeetu7/Idris2 into jeetu7-master Edwin Brady 2020-04-21 10:47:38 +0100
  • ac277ce6d0 Erase the World, with care Edwin Brady 2020-04-21 10:42:00 +0100
  • 5ea11cf0f5
         Merge pull request #282 from abailly/network-binary Edwin Brady 2020-04-21 10:45:52 +0100
  • d3d5e22011
         Merge pull request #274 from ska80/tutorial/typos Edwin Brady 2020-04-21 10:39:53 +0100
  • 4b65d8d6fc
         Merge pull request #273 from jfdm/badges Edwin Brady 2020-04-21 10:39:09 +0100
  • db7bbb62db Fix some named-interface stuff Fabián Heredia Montiel 2020-04-17 22:20:11 -0500
  • 7cd9964d4f Comment correction Edwin Brady 2020-04-19 23:45:30 +0100
  • f6bbfb3dee Remove costly 'swapBlocks' in lambda lifter Edwin Brady 2020-04-19 23:41:24 +0100
  • 1734841275 Add a lambda lifter Edwin Brady 2020-04-19 22:56:21 +0100
  • 8fccd5f2a3 Properly erase constructor arguments Edwin Brady 2020-04-19 19:43:51 +0100
  • 44c01f83d2 Move outermost lambdas to top level Edwin Brady 2020-04-19 16:49:25 +0100
  • ae6e7a7d95 Fix record projections. Matus Tejiscak 2020-04-19 00:35:34 +0200
  • 4d2b270db6 Allow spaces in file path for generated Chez programs Christian Rasmussen 2019-09-06 01:47:00 +0200
  • f37d69ceb7 Add tests/idris2/record003. Matus Tejiscak 2020-04-18 14:04:30 +0200
  • b977bc1974 Fix dotted getters in parameters blocks. Matus Tejiscak 2020-04-18 13:56:51 +0200
  • ae8e9c5f6d Use a local function to parse names. Matus Tejiscak 2020-04-18 12:52:00 +0200
  • 2d02899679 Adjust some tests. Matus Tejiscak 2020-04-18 12:19:17 +0200
  • 3e398584b3 Print non-namespaced idents backwards-compatibly. Matus Tejiscak 2020-04-18 12:00:23 +0200
  • f834c283ea Use pragmas in the TTImp parser. Matus Tejiscak 2020-04-18 11:49:15 +0200
  • d30c108a9b Print record updates with dots. Matus Tejiscak 2020-04-18 11:41:33 +0200
  • a997a4b8fe Make the record update syntax use dots. Matus Tejiscak 2020-04-18 11:38:45 +0200
  • d1bcb124b6 More fixes. Matus Tejiscak 2020-04-18 10:01:19 +0200
  • 77ab7a26bc remove ^ and use #: instead Soham Chowdhury 2020-04-18 02:23:35 +0000
  • c53e675c33 Add %undotted_record_projections pragma. Matus Tejiscak 2020-04-18 01:10:56 +0200
  • 3469e033ed Disambiguate RF and UN properly. Matus Tejiscak 2020-04-18 00:53:12 +0200
  • 8a0d1b29c7 Also generate old-style projections. Matus Tejiscak 2020-04-18 00:35:24 +0200
  • 32de5f0966 Enable Namespace.(.field). Matus Tejiscak 2020-04-18 00:22:16 +0200
  • b745ec0e8b Fix userNameRoot. Matus Tejiscak 2020-04-17 23:13:40 +0200
  • 85019a75d9 More fixups. Matus Tejiscak 2020-04-17 22:48:54 +0200
  • c36250f271 Fix operator names. Matus Tejiscak 2020-04-17 21:55:49 +0200
  • c450d82087 Fix keywords. Matus Tejiscak 2020-04-17 21:51:10 +0200
  • 6987685b55 Lex pragmas separately. Matus Tejiscak 2020-04-17 21:32:39 +0200
  • 898095a074 More fixups. Matus Tejiscak 2020-04-17 21:17:07 +0200
  • ab04e95ce7 Specialise dotted namespaces as lexemes. Matus Tejiscak 2020-04-17 20:08:56 +0200
  • e4a5c7d167 add args back and render toplevel term Soham Chowdhury 2020-04-17 15:36:31 +0000
  • 9061aee9da complete texttt in a way that the parser can read Soham Chowdhury 2020-04-17 14:02:43 +0000
  • 767d9dc5f3 Add tests for default implict record type arguments Ohad Kammar 2020-04-17 12:22:36 +0100
  • 5af82beb4e bugfix: actually include keyword "default" for default implict record type arguments Ohad Kammar 2020-04-17 12:07:20 +0100
  • 3043ac0be4 Add support for default implicit arguments in record types Ohad Kammar 2020-04-17 10:28:51 +0100
  • f777531f52 Merge branch 'master' of github.com:edwinb/Idris2 into fully-abstract-records Ohad Kammar 2020-04-17 09:06:02 +0100
  • 1fcac7a144 Add commits back to parser, simplify case-split for (auto)implict arguments in records Ohad Kammar 2020-04-17 09:04:59 +0100
  • c5070eba19 Bugfix: In mapPTerm, correctly handle the parameter list in a PRecord Ohad Kammar 2020-04-17 08:36:41 +0100
  • 7ddf1b9818 Use an arrow for record fields. Matus Tejiscak 2020-04-17 01:34:19 +0200
  • 86d308da12 Fix names of projections. Matus Tejiscak 2020-04-17 01:04:48 +0200
  • e8166c2dc8 Fix schName. Matus Tejiscak 2020-04-17 00:50:38 +0200
  • ef826ff45c Use RF names for record projections. Matus Tejiscak 2020-04-17 00:44:53 +0200
  • 4b986e8b61 Fix record dot syntax parser. Matus Tejiscak 2020-04-17 00:35:39 +0200
  • ca1ef8a882 Implement record dot syntax as Idris sugar. Matus Tejiscak 2020-04-17 00:21:12 +0200
  • 10f9d02ecd Implement dot record syntax. Matus Tejiscak 2020-04-16 23:37:45 +0200
  • 884d4adad2 Fix buffer allocation error Edwin Brady 2020-04-16 22:17:01 +0100
  • 801da788ed Add the RecordProjection lexeme. Matus Tejiscak 2020-04-16 22:47:21 +0200
  • 2e0002535a Merge branch 'master' into casetree Guillaume Allais 2020-04-16 15:52:59 +0100
  • 1b74c5fde4 [ cleanup ] removing a lot of useless polymorphism Guillaume Allais 2020-04-16 14:54:22 +0100
  • 9bc72a79c0 Need 'begin' around putstr primitive Edwin Brady 2020-04-16 13:59:23 +0100
  • 40980786e1 Ignoring the World is inadvisable Edwin Brady 2020-04-16 13:39:55 +0100
  • dfc7001bfc Ditto Kamil Shakirov 2020-04-16 18:23:13 +0600
  • 58ded85934 Merge remote-tracking branch 'upstream' Soham Chowdhury 2020-04-16 02:08:24 +0000
  • 73d2e7bc29 Merge branch 'master' of github.com:edwinb/Idris2 into fully-abstract-records Ohad Kammar 2020-04-16 02:50:06 +0100
  • aa451022b5 Add tests for fully abstract records in Idris and Yaffle Ohad Kammar 2020-04-16 02:49:32 +0100
  • 43634e3e01 Add support for record auto implicit parameters in parser Ohad Kammar 2020-04-16 02:47:17 +0100
  • cef456fa54 Bugfix: differentiate between implicit and explicit arguments in the return type of the constructor Ohad Kammar 2020-04-16 01:49:00 +0100
  • e6be2af83d Add syntax for implicit arguments to records Ohad Kammar 2020-04-16 01:07:47 +0100
  • b665e6afbf Another small inlining improvement Edwin Brady 2020-04-15 23:59:54 +0100
  • 0a7d94babc
         Fix Idris1 download link George Pollard 2020-04-16 08:58:08 +1200
  • 048bce23a6 Make inlining faster with One Weird Trick Edwin Brady 2020-04-15 21:46:28 +0100
  • 8eabc27dac [ refactor ] boolean expression Guillaume Allais 2020-04-15 20:55:18 +0100
  • 95da5a8b74 Refactor to allow supporting implicit and rit annotations on records (without adding syntax for them) Ohad Kammar 2020-04-15 18:30:26 +0100
  • eabb23f8ce [ refactor ] remove redundant check isLet Guillaume Allais 2020-04-15 13:41:04 +0100
  • 10a791c09a Fix Coredris backend after NamedCExp changes Soham Chowdhury 2020-04-15 18:24:39 +0530
  • 9152caded1 [ cleanup ] use reverseOnto Guillaume Allais 2020-04-15 10:45:17 +0100
  • 3ae4267de9 [ refactor ] following discussion with @ziman Guillaume Allais 2020-04-13 11:30:42 +0100
  • b60fdf2c0d [ doc ] for the case tree constructors Guillaume Allais 2020-04-13 11:30:20 +0100
  • 5c957563b6 Merge remote-tracking branch 'refs/remotes/origin/master' Soham Chowdhury 2020-04-15 11:08:49 +0000
  • 0779924c2a coredris: init Soham Chowdhury 2020-04-15 11:08:35 +0000
  • d5bfb8f136 Use explicit named representation for compiling Edwin Brady 2020-04-15 11:14:02 +0100
  • 5544919c31 use quotient on scheme backends Arnaud Bailly 2020-04-15 10:52:35 +0200
  • 0254ff109c Merge branch 'master' of github.com:edwinb/Idris2 into fully-abstract-records Ohad Kammar 2020-04-15 08:46:12 +0100
  • 41ef3fdd2a Don't use exact-floor in cast-string-int. Matus Tejiscak 2020-04-14 21:38:45 +0200
  • c3b6b130fd Also fix up cast-string-int. Matus Tejiscak 2020-04-14 20:02:20 +0200
  • 7a3ebd9a2f Use exact-floor. Matus Tejiscak 2020-04-14 19:57:09 +0200
  • 18962eeacf Fix casting in integral division. Matus Tejiscak 2020-04-14 19:39:18 +0200