Code

General inductive parameters#2506

Code

Merged

jonaprieto merged 69 commits intomainanoma/juvix:mainfrom inductive-parameters-2anoma/juvix:inductive-parameters-2Copy head branch name to clipboardNov 15, 2023

+545-102

Commits

Commits on Sep 13, 2023

• Squashed commit of the following:

  Show description for 423894a
  janmasrovira

  committed
  423894a

  Copy full SHA for 423894a

• wip

  janmasrovira

  committed
  1f67f1e

  Copy full SHA for 1f67f1e

• add Functor test

  janmasrovira

  committed
  d807e4d

  Copy full SHA for d807e4d

• debugging

  janmasrovira

  committed
  203aa20

  Copy full SHA for 203aa20

• match arities

  janmasrovira

  committed
  ed98613

  Copy full SHA for ed98613

• improve arity checker

  janmasrovira

  committed
  ed5a994

  Copy full SHA for ed5a994

• improve arity heuristics

  janmasrovira

  committed
  742168a

  Copy full SHA for 742168a

• extend test

  janmasrovira

  committed
  7659741

  Copy full SHA for 7659741

• change name to avoid warning

  janmasrovira

  committed
  4c796df

  Copy full SHA for 4c796df

• remove TODO

  janmasrovira

  committed
  4fdb2eb

  Copy full SHA for 4fdb2eb

• revert name

  janmasrovira

  committed
  5a45dbc

  Copy full SHA for 5a45dbc

• remove traces

  janmasrovira

  committed
  3d6f30f

  Copy full SHA for 3d6f30f

• remove TODO

  janmasrovira

  committed
  c87651b

  Copy full SHA for c87651b

• add test to suite

  janmasrovira

  committed
  efc6af0

  Copy full SHA for efc6af0

• revert arity changes

  janmasrovira

  committed
  ce6edfc

  Copy full SHA for ce6edfc

• Merge remote-tracking branch 'origin/main' into inductive-parameters

  janmasrovira

  committed
  4d352fa

  Copy full SHA for 4d352fa

Commits on Sep 14, 2023

• revert change

  janmasrovira

  committed
  67d69a0

  Copy full SHA for 67d69a0

• Merge remote-tracking branch 'origin/main' into inductive-parameters

  janmasrovira

  committed
  8186adb

  Copy full SHA for 8186adb

• update to new fixity syntax

  janmasrovira

  committed
  512715f

  Copy full SHA for 512715f

• Merge remote-tracking branch 'origin/main' into inductive-parameters

  janmasrovira

  committed
  0d6bc69

  Copy full SHA for 0d6bc69

• remove dead code

  janmasrovira

  committed
  d892c57

  Copy full SHA for d892c57

• add isParamImplicitOrInstance definition

  janmasrovira

  committed
  802398c

  Copy full SHA for 802398c

• fix type of holes

  janmasrovira

  committed
  94588af

  Copy full SHA for 94588af

• Merge remote-tracking branch 'origin/main' into inductive-parameters

  janmasrovira

  committed
  9082b14

  Copy full SHA for 9082b14

Commits on Nov 6, 2023

• wip

  janmasrovira

  committed
  0bd2397

  Copy full SHA for 0bd2397

• add holes in application

  janmasrovira

  committed
  0bd358c

  Copy full SHA for 0bd358c

• recurse addHole

  janmasrovira

  committed
  e0bc03d

  Copy full SHA for e0bc03d

• trailing holes

  janmasrovira

  committed
  2265d82

  Copy full SHA for 2265d82

• revert default algorithm

  janmasrovira

  committed
  ae2cfc8

  Copy full SHA for ae2cfc8

• fix fold application

  janmasrovira

  committed
  96bf0d5

  Copy full SHA for 96bf0d5

• insert wildcards

  janmasrovira

  committed
  0b9c250

  Copy full SHA for 0b9c250

• wip

  janmasrovira

  committed
  96dd07e

  Copy full SHA for 96dd07e

• wip

  janmasrovira

  committed
  835a709

  Copy full SHA for 835a709

• clean

  janmasrovira

  committed
  37ac7a0

  Copy full SHA for 37ac7a0

• add CastHole

  janmasrovira

  committed
  66d2de0

  Copy full SHA for 66d2de0

• fix builder

  janmasrovira

  committed
  444c60f

  Copy full SHA for 444c60f

• add tests

  janmasrovira

  committed
  fb313e6

  Copy full SHA for fb313e6

• hint

  janmasrovira

  committed
  c9fb613

  Copy full SHA for c9fb613

• adjust holes

  janmasrovira

  committed
  6b61073

  Copy full SHA for 6b61073

• fix

  janmasrovira

  committed
  de4eed9

  Copy full SHA for de4eed9

• restrict type synonyms to unnamed arguments

  janmasrovira

  committed
  02721d4

  Copy full SHA for 02721d4

Commits on Nov 7, 2023

• wip InstanceHole

  janmasrovira

  committed
  bb81b77

  Copy full SHA for bb81b77

• Merge remote-tracking branch 'origin/main' into 2362-interleave-arity-and-type-checking

  janmasrovira

  committed
  7684a7e

  Copy full SHA for 7684a7e

• separate InstanceHole from normal Hole

  janmasrovira

  committed
  0a8be4b

  Copy full SHA for 0a8be4b

• lenses

  janmasrovira

  committed
  e6e0f36

  Copy full SHA for e6e0f36

• adapt termination

  janmasrovira

  committed
  86ed19f

  Copy full SHA for 86ed19f

Commits on Nov 8, 2023

• remove canBeUniverse

  janmasrovira

  committed
  6c13b74

  Copy full SHA for 6c13b74

• Merge remote-tracking branch 'origin/main' into 2362-interleave-arity-and-type-checking

  janmasrovira

  committed
  8a192e6

  Copy full SHA for 8a192e6

• Merge branch 'inductive-parameters' into inductive-parameters-2

  janmasrovira

  committed
  3a51d35

  Copy full SHA for 3a51d35

• update name signature builder for inductive types

  janmasrovira

  committed
  6a0c89a

  Copy full SHA for 6a0c89a

• uncomment instances

  janmasrovira

  committed
  bb332e5

  Copy full SHA for bb332e5

• add Reader monad

  janmasrovira

  committed
  ccf52a6

  Copy full SHA for ccf52a6

Commits on Nov 9, 2023

• update test

  janmasrovira

  committed
  53609ff

  Copy full SHA for 53609ff

• remove traces

  janmasrovira

  committed
  47c02ca

  Copy full SHA for 47c02ca

• add tests

  janmasrovira

  committed
  3d5b159

  Copy full SHA for 3d5b159

• clean

  janmasrovira

  committed
  a0c520a

  Copy full SHA for a0c520a

• clean

  janmasrovira

  committed
  a79b5b5

  Copy full SHA for a79b5b5

• revert canBeUniverse

  janmasrovira

  committed
  664af9e

  Copy full SHA for 664af9e

• Merge branch '2362-interleave-arity-and-type-checking' into inductive-parameters-2

  janmasrovira

  committed
  bd8713c

  Copy full SHA for bd8713c

Commits on Nov 10, 2023

• add arity checking for builtins

  janmasrovira

  committed
  ee23caf

  Copy full SHA for ee23caf

• Merge branch '2362-interleave-arity-and-type-checking' into inductive-parameters-2

  janmasrovira

  committed
  60021e4

  Copy full SHA for 60021e4

• add canBeUniverse

  janmasrovira

  committed
  d8fce2b

  Copy full SHA for d8fce2b

Commits on Nov 11, 2023

• add monad tests

  janmasrovira

  committed
  3d40541

  Copy full SHA for 3d40541

Commits on Nov 12, 2023

• extend ReaderT

  janmasrovira

  committed
  2595774

  Copy full SHA for 2595774

• empty commit

  janmasrovira

  committed
  661f0d6

  Copy full SHA for 661f0d6

Commits on Nov 13, 2023

• Merge branch 'main' into inductive-parameters-2

  janmasrovira

  committed
  38610f8

  Copy full SHA for 38610f8

• Merge remote-tracking branch 'origin/main' into inductive-parameters-2

  janmasrovira

  committed
  17504e0

  Copy full SHA for 17504e0

• add tests

  janmasrovira

  committed
  006d9ca

  Copy full SHA for 006d9ca

Commits on Nov 14, 2023

• Merge branch 'main' into inductive-parameters-2

  lukaszcz

  authored
  bdb4011

  Copy full SHA for bdb4011