Code

Typeclass lang#76

Code

Merged

hrutvik merged 175 commits intomasterCakeML/pure:masterfrom typeclassLangCakeML/pure:typeclassLangCopy head branch name to clipboardDec 30, 2024

+21,601

Commits

Commits on Oct 7, 2023

• typeclass parsing: copy parsing from pure and change pureAST

  Gordon-Sau

  committed
  9dbda8c

  Copy full SHA for 9dbda8c

• typeclass typing: copy pure_tcexp and pure_typing

  Show description for b9a03e7
  Gordon-Sau

  committed
  b9a03e7

  Copy full SHA for b9a03e7

• Merge remote-tracking branch 'origin/master' into typeclassLang

  Gordon-Sau

  committed
  88a2a9e

  Copy full SHA for 88a2a9e

Commits on Oct 8, 2023

• typeclass kind_check: add an inductive set for kind_checking

  Gordon-Sau

  committed
  1225587

  Copy full SHA for 1225587

Commits on Oct 17, 2023

• typeclass: fixing holmake errors

  Gordon-Sau

  committed
  8bd5a3a

  Copy full SHA for 8bd5a3a

Commits on Nov 15, 2023

• typeclass: update type system, add kind check and pure_tcexp

  Gordon-Sau

  committed
  5301eac

  Copy full SHA for 5301eac

• typeclass: update AST to support class and instance declarations

  Gordon-Sau

  committed
  e9be6bf

  Copy full SHA for e9be6bf

Commits on Nov 25, 2023

• typeclass: complete most of ast_to_cexp

  Gordon-Sau

  committed
  00d42de

  Copy full SHA for 00d42de

Commits on Nov 27, 2023

• typeclass: add helper functions and lemmas in tcexp

  Gordon-Sau

  committed
  199ad32

  Copy full SHA for 199ad32

• typeclass: update ast_to_cexp

  Gordon-Sau

  committed
  792c135

  Copy full SHA for 792c135

Commits on Nov 28, 2023

• tcexp: remove unnecessary keys in instinfo

  Gordon-Sau

  committed
  68f8463

  Copy full SHA for 68f8463

• ast_to_cexp: transform all usage of finite map to mlmap

  Gordon-Sau

  committed
  f672e3f

  Copy full SHA for f672e3f

Commits on Dec 12, 2023

• Move letrecs_distinct_def and Lets_def up

  

  myreen

  authored and

  Gordon-Sau

  committed
  3e750b8

  Copy full SHA for 3e750b8

• Make letrecs_distinct_def into an automatic simp

  

  myreen

  authored and

  Gordon-Sau

  committed
  b1b1552

  Copy full SHA for b1b1552

• Move some definitions upwards

  

  myreen

  authored and

  Gordon-Sau

  committed
  600e940

  Copy full SHA for 600e940

• Delete some unnecessary dependencies in pure_tcexpTheory

  

  hrutvik

  authored and

  Gordon-Sau

  committed
  7e97a54

  Copy full SHA for 7e97a54

• Update translation for moves

  

  myreen

  authored and

  Gordon-Sau

  committed
  a784aad

  Copy full SHA for a784aad

• Tweak pure_pres

  

  myreen

  authored and

  Gordon-Sau

  committed
  b56f03b

  Copy full SHA for b56f03b

• Tidy up some thunkLang files

  

  myreen

  authored and

  Gordon-Sau

  committed
  55fceea

  Copy full SHA for 55fceea

• Fix App_Lam rule in bidir

  

  myreen

  authored and

  Gordon-Sau

  committed
  b1dee19

  Copy full SHA for b1dee19

• Fix a broken proof (in an unused file)

  

  myreen

  authored and

  Gordon-Sau

  committed
  4b2d955

  Copy full SHA for 4b2d955

• Pass in numbers on command line

  

  hrutvik

  authored and

  Gordon-Sau

  committed
  d8e147e

  Copy full SHA for d8e147e

• Fix a breakage

  

  hrutvik

  authored and

  Gordon-Sau

  committed
  cb19eaf

  Copy full SHA for cb19eaf

• Remove some test code

  

  hrutvik

  authored and

  Gordon-Sau

  committed
  f706862

  Copy full SHA for f706862

• Delete unused things

  

  myreen

  authored and

  Gordon-Sau

  committed
  604c23c

  Copy full SHA for 604c23c

• Remove Rec and rename to inline_rel

  

  myreen

  authored and

  Gordon-Sau

  committed
  6be18ed

  Copy full SHA for 6be18ed

• Remove rhs type

  

  myreen

  authored and

  Gordon-Sau

  committed
  60ffb5e

  Copy full SHA for 60ffb5e

• Replace Binds with Lets

  

  myreen

  authored and

  Gordon-Sau

  committed
  0795695

  Copy full SHA for 0795695

• Define pre and tidy up proofs

  

  myreen

  authored and

  Gordon-Sau

  committed
  6a549da

  Copy full SHA for 6a549da

• Remove boundvars from vars_of

  

  myreen

  authored and

  Gordon-Sau

  committed
  0707363

  Copy full SHA for 0707363

• Switch to using pure_inline_relTheory

  

  myreen

  authored and

  Gordon-Sau

  committed
  d4fb191

  Copy full SHA for d4fb191

• Delete crhs type and update proofs

  

  myreen

  authored and

  Gordon-Sau

  committed
  ba31a73

  Copy full SHA for ba31a73

• Tidy up definition of inline_rel

  

  myreen

  authored and

  Gordon-Sau

  committed
  f410a0b

  Copy full SHA for f410a0b

• Rearrange content of file

  

  myreen

  authored and

  Gordon-Sau

  committed
  39c8be8

  Copy full SHA for 39c8be8

• Simplify pre

  

  myreen

  authored and

  Gordon-Sau

  committed
  88f0575

  Copy full SHA for 88f0575

• Clean up the inliner implementation

  Show description for 18b3c4f
  

  KacperFKorban

  authored and

  Gordon-Sau

  committed
  18b3c4f

  Copy full SHA for 18b3c4f

• Remove named TODOs

  

  KacperFKorban

  authored and

  Gordon-Sau

  committed
  50f66ff

  Copy full SHA for 50f66ff

• Define lets_ok as in paper

  

  myreen

  authored and

  Gordon-Sau

  committed
  f0d8e49

  Copy full SHA for f0d8e49

• Switch to using remove_call_arg name (as in paper)

  

  myreen

  authored and

  Gordon-Sau

  committed
  c3a3100

  Copy full SHA for c3a3100

• Alternative definitions of specialisation

  

  hrutvik

  authored and

  Gordon-Sau

  committed
  d431bc6

  Copy full SHA for d431bc6

• Add inlining to benchmarking config

  

  hrutvik

  authored and

  Gordon-Sau

  committed
  15d044b

  Copy full SHA for 15d044b

• Update examples README with inlining

  

  hrutvik

  authored and

  Gordon-Sau

  committed
  181938c

  Copy full SHA for 181938c

• Delete no_shadowing (replace with barendregt)

  

  myreen

  authored and

  Gordon-Sau

  committed
  aad8425

  Copy full SHA for aad8425

• Update for rebind

  

  myreen

  authored and

  Gordon-Sau

  committed
  0b357c3

  Copy full SHA for 0b357c3

• Remove some duplicates

  

  myreen

  authored and

  Gordon-Sau

  committed
  6e9ca0b

  Copy full SHA for 6e9ca0b

• Updates for rebind

  

  myreen

  authored and

  Gordon-Sau

  committed
  cf1bac4

  Copy full SHA for cf1bac4

• Fixes for rebind

  

  myreen

  authored and

  Gordon-Sau

  committed
  e85a889

  Copy full SHA for e85a889

• Fix rebinds

  

  myreen

  authored and

  Gordon-Sau

  committed
  8350da7

  Copy full SHA for 8350da7

• Fix rebinds

  

  myreen

  authored and

  Gordon-Sau

  committed
  8b6e8e6

  Copy full SHA for 8b6e8e6

• Add relations dir to top-level Holmakefile

  

  myreen

  authored and

  Gordon-Sau

  committed
  6fe323a

  Copy full SHA for 6fe323a

• Fix rebinds

  

  myreen

  authored and

  Gordon-Sau

  committed
  76d8822

  Copy full SHA for 76d8822

• Update CI: longer timeout + build new relations directory

  

  hrutvik

  authored and

  Gordon-Sau

  committed
  1b6cdb0

  Copy full SHA for 1b6cdb0

• Update benchmarking patches

  

  hrutvik

  authored and

  Gordon-Sau

  committed
  de718bd

  Copy full SHA for de718bd

• Add a script for updating files to adjusted syntax of Inductive

  

  myreen

  authored and

  Gordon-Sau

  committed
  246d8e7

  Copy full SHA for 246d8e7

• Fix for adjusted Inductive syntax in HOL

  

  myreen

  authored and

  Gordon-Sau

  committed
  8bdb3a4

  Copy full SHA for 8bdb3a4

• Fix for adjusted Inductive syntax

  

  myreen

  authored and

  Gordon-Sau

  committed
  88e5899

  Copy full SHA for 88e5899

• Get a file to build

  

  myreen

  authored and

  Gordon-Sau

  committed
  24757ce

  Copy full SHA for 24757ce

• Fix for new case_elim in HOL (HOL-Theorem-Prover/HOL@64ee5d9)

  

  hrutvik

  authored and

  Gordon-Sau

  committed
  1ff186c

  Copy full SHA for 1ff186c

• Fixes for OPTREL changes in HOL (probably HOL-Theorem-Prover/HOL@f0a4649)

  

  hrutvik

  authored and

  Gordon-Sau

  committed
  88588bb

  Copy full SHA for 88588bb

• typeclass: ast_to_cexp: reject duplicate function definition and create signature map

  Gordon-Sau

  committed
  b3c7d68

  Copy full SHA for b3c7d68

• remove /\ in kind_wf definition

  Gordon-Sau

  committed
  1110f32

  Copy full SHA for 1110f32

Commits on Dec 26, 2023

• typeclass: add wellformedness check (TODO)

  Gordon-Sau

  committed
  57c1337

  Copy full SHA for 57c1337

Commits on Feb 9, 2024

• typeclassLang: update the prefix to "typeclass_" and update well-formedness and kind check

  Gordon-Sau

  committed
  6a88061

  Copy full SHA for 6a88061

• typeclassLang: move the implementations of maps for type classes and instances to a separate file

  Gordon-Sau

  committed
  fb6a859

  Copy full SHA for fb6a859

• typeclassLang: implement a generic cycle detection algorithm

  Gordon-Sau

  committed
  4c908f6

  Copy full SHA for 4c908f6

• typeclassLang: implement cycle detection for typeclass superclass relation

  Gordon-Sau

  committed
  640359c

  Copy full SHA for 640359c

Commits on Feb 10, 2024

• typeclass: change the proof for cycle_detection to use TC_depends_on_weak

  Gordon-Sau

  committed
  4a8dc58

  Copy full SHA for 4a8dc58

Commits on Feb 16, 2024

• typeclassLang: attempt to update unification

  Gordon-Sau

  committed
  53671c8

  Copy full SHA for 53671c8

• typeclass: update datatype for type

  Gordon-Sau

  committed
  e3020bf

  Copy full SHA for e3020bf

Commits on Feb 17, 2024

• half way through unification

  Gordon-Sau

  committed
  1620167

  Copy full SHA for 1620167

Commits on Feb 20, 2024

• unification done

  Gordon-Sau

  committed
  98bc413

  Copy full SHA for 98bc413

Commits on Mar 5, 2024

• typeclass: prove termination of by_super

  Gordon-Sau

  committed
  26bc7e2

  Copy full SHA for 26bc7e2

Commits on Mar 19, 2024

• typeclass: update definition of by_super

  Gordon-Sau

  committed
  b67b99b

  Copy full SHA for b67b99b

• typeclass: complete by_super_aux termination proof

  Gordon-Sau

  committed
  ff88baa

  Copy full SHA for ff88baa

• typeclass_env_map: prove by_super implies super_reachable

  Gordon-Sau

  committed
  150e9ad

  Copy full SHA for 150e9ad

Commits on Mar 21, 2024

• typeclass_env_map: make by_super_IMP_reachable stronger

  Gordon-Sau

  committed
  1b4bb16

  Copy full SHA for 1b4bb16

• typeclass_env_map: prove that if something is reachable, then it is visited by by_super_aux

  Gordon-Sau

  committed
  e24f755

  Copy full SHA for e24f755

• type_env_map: prove that by_super_aux is equivalent to super_reachable

  Gordon-Sau

  committed
  bb2d2fd

  Copy full SHA for bb2d2fd

• typeclas_env_map: prove that if the cl_map is well_formed, then by_super only needs to check the class is in the map

  Gordon-Sau

  committed
  73686ef

  Copy full SHA for 73686ef

Commits on Apr 4, 2024

• update instance syntax and inst_map

  Gordon-Sau

  committed
  c492569

  Copy full SHA for c492569

• typeclass_env_map: add init_inst_map and inst_map_cmp (the comparison function for init_inst_map)

  Gordon-Sau

  committed
  6c0e7fd

  Copy full SHA for 6c0e7fd

• typeclass: fix ast_to_cexp

  Gordon-Sau

  committed
  bf6eef8

  Copy full SHA for bf6eef8

• typeclass_env_map: add by_inst

  Gordon-Sau

  committed
  4a920ce

  Copy full SHA for 4a920ce

• typeclass_env_map: add some entail theorems

  Gordon-Sau

  committed
  20c3dae

  Copy full SHA for 20c3dae

• typeclass_types: add tcons_to_type to typeclass_types

  Show description for f190511
  Gordon-Sau

  committed
  f190511

  Copy full SHA for f190511

Commits on Apr 5, 2024

• typeclass: refactroring, update spec and typing rules

  Gordon-Sau

  committed
  808c588

  Copy full SHA for 808c588

Commits on Apr 13, 2024

• typeclass_typing: update typing and class constraint elaboration rules

  Gordon-Sau

  committed
  10a7dd8

  Copy full SHA for 10a7dd8

• typeclass_typing: add typing rules for Prim

  Gordon-Sau

  committed
  9473173

  Copy full SHA for 9473173

• typeclass_typing: add typing rules for NestedCases

  Gordon-Sau

  committed
  800f7a2

  Copy full SHA for 800f7a2

Commits on Apr 14, 2024

• typeclass_typing: prove kind is preserved under substitution and typing rules implies the dictionary is constructible

  Gordon-Sau

  committed
  5d504e1

  Copy full SHA for 5d504e1

Commits on Apr 15, 2024

• typeclass_typing: implement translation of predicate (termination proof with acyclic_depth)

  Gordon-Sau

  committed
  f3a1220

  Copy full SHA for f3a1220

Commits on Apr 17, 2024

• typeclass pure_tcexp: updatepure_tcexp with Nestedcase

  Gordon-Sau

  committed
  5f2d7e2

  Copy full SHA for 5f2d7e2

• typeclass typing: renamce typeclass_tcexp to texp and add exhausive check for pattern matching

  Gordon-Sau

  committed
  7e9d23c

  Copy full SHA for 7e9d23c

• typeclass pure_tcexp: add NestedCase to pure_tcexp and update lemmas about pure_tcexp

  Gordon-Sau

  committed
  91c2c19

  Copy full SHA for 91c2c19

Commits on Apr 18, 2024

• typeclass tcexp: add the check that case pattern does not contain the varibale name of the expression we are casing on to tcexp_wf

  Gordon-Sau

  committed
  c0fb2f7

  Copy full SHA for c0fb2f7

• typeclass typing: update typing rules for tcexp

  Gordon-Sau

  committed
  8897617

  Copy full SHA for 8897617

Commits on Apr 19, 2024

• typeclass typing: update translate pred types related stuffs

  Gordon-Sau

  committed
  251021c

  Copy full SHA for 251021c

Commits on May 10, 2024

• update pure_tcexp_typing

  Gordon-Sau

  committed
  2a99f72

  Copy full SHA for 2a99f72

• add type_elaborate_prog

  Gordon-Sau

  committed
  9c5bd61

  Copy full SHA for 9c5bd61

Commits on May 11, 2024

• implement prog_construct_dict

  Gordon-Sau

  committed
  878f16e

  Copy full SHA for 878f16e

Commits on May 12, 2024

• fix class_env_to_env

  Gordon-Sau

  committed
  ffe7eec

  Copy full SHA for ffe7eec

Commits on May 13, 2024

• type_check foldMap

  Gordon-Sau

  committed
  3279f7a

  Copy full SHA for 3279f7a

• type_check foldMap and mappend for list

  Gordon-Sau

  committed
  7eaf764

  Copy full SHA for 7eaf764

Commits on May 14, 2024

• type chest example

  Gordon-Sau

  committed
  153433c

  Copy full SHA for 153433c

Commits on May 15, 2024

• prove type_elaborate example with default methods

  Gordon-Sau

  committed
  f2415e8

  Copy full SHA for f2415e8

Commits on May 16, 2024

• typecheck example with instances with constraints

  Gordon-Sau

  committed
  5c75063

  Copy full SHA for 5c75063

Commits on May 17, 2024

• fix super class translationg in instance_construct_dict

  Gordon-Sau

  committed
  5df4527

  Copy full SHA for 5df4527

Commits on May 18, 2024

• use SmartLam and prove test_instance_env_construct_dict

  Gordon-Sau

  committed
  9e3adc8

  Copy full SHA for 9e3adc8

Commits on May 19, 2024

• move thms to the right places

  Gordon-Sau

  committed
  f9c7615

  Copy full SHA for f9c7615

Commits on May 22, 2024

• fixing typingProps

  Gordon-Sau

  committed
  2837f1b

  Copy full SHA for 2837f1b

Commits on May 26, 2024

• fixing typing rules for typeclass lang and proving props for the typing rules

  Gordon-Sau

  committed
  a626da6

  Copy full SHA for a626da6

• add some theorems in typeclass_kindCheck and typeclass_texp

  Gordon-Sau

  committed
  021ec94

  Copy full SHA for 021ec94

• add itype_kind_ok to inference_common

  Gordon-Sau

  committed
  7582f36

  Copy full SHA for 7582f36

• move theorems from typeclass_env_map_impl to typeclass_typesProps

  Gordon-Sau

  committed
  5fd8a16

  Copy full SHA for 5fd8a16

• fix typeclass typing rules example

  Gordon-Sau

  committed
  4c398db

  Copy full SHA for 4c398db

Commits on May 27, 2024

• fixing typing rules

  Gordon-Sau

  committed
  662c969

  Copy full SHA for 662c969

Commits on May 29, 2024

• fix pure_tcexp_typing Case rule and prove type_ok

  Gordon-Sau

  committed
  91048ed

  Copy full SHA for 91048ed

Commits on Jun 9, 2024

• prove type_tcexp_subst_db

  Gordon-Sau

  committed
  48e9ecc

  Copy full SHA for 48e9ecc

• proving shift_db

  Gordon-Sau

  committed
  57de8ee

  Copy full SHA for 57de8ee

• proved type_tcxp_shift_db

  Gordon-Sau

  committed
  781cd16

  Copy full SHA for 781cd16

Commits on Jun 10, 2024

• prove freevars_specialises

  Gordon-Sau

  committed
  57e6d06

  Copy full SHA for 57e6d06

Commits on Jun 11, 2024

• update Seq rule for insert_seq

  Gordon-Sau

  committed
  f67a54e

  Copy full SHA for f67a54e

Commits on Jun 13, 2024

• Proves that insert_seq preserves typing and updated proofs that breaks due to the new seq typing rules

  Gordon-Sau

  committed
  156e185

  Copy full SHA for 156e185

• update typesoundness proofs with some cheats

  Gordon-Sau

  committed
  f07fcca

  Copy full SHA for f07fcca

Commits on Jun 17, 2024

• Fix a theory name

  Show description for fe6a9d0
  IlmariReissumies

  committed
  fe6a9d0

  Copy full SHA for fe6a9d0

• Fix another theory name

  IlmariReissumies

  committed
  a129727

  Copy full SHA for a129727

• Fix some more theory names

  IlmariReissumies

  committed
  9762758

  Copy full SHA for 9762758

Commits on Jun 18, 2024

• Prove some "easy" cases from type_soundness_up_to

  IlmariReissumies

  committed
  825eb84

  Copy full SHA for 825eb84

• Use >~ instead of comments to signpost

  IlmariReissumies

  committed
  c32b0df

  Copy full SHA for c32b0df

• Prove Apps case

  IlmariReissumies

  committed
  d7f961f

  Copy full SHA for d7f961f

• Prove Letrec case

  IlmariReissumies

  committed
  217516e

  Copy full SHA for 217516e

• start working on dictionary construction proof

  Gordon-Sau

  committed
  a7cba93

  Copy full SHA for a7cba93

Commits on Jun 21, 2024

• adding distinctness conditions

  Gordon-Sau

  committed
  050fd95

  Copy full SHA for 050fd95

Commits on Jun 22, 2024

• prove the var and pred case

  Gordon-Sau

  committed
  c90d6ad

  Copy full SHA for c90d6ad

• working on Let rule and found that we need to shift lie when we are generalizing

  Gordon-Sau

  committed
  91d777d

  Copy full SHA for 91d777d

Commits on Jun 23, 2024

• tshift the lie in the typing rules

  Gordon-Sau

  committed
  9a4124a

  Copy full SHA for 9a4124a

• typeclass: texp_construct_dict_type_tcexp: prove Let and Lam case

  Gordon-Sau

  committed
  62e71d9

  Copy full SHA for 62e71d9

Commits on Jun 24, 2024

• Cons

  Gordon-Sau

  committed
  9fd797d

  Copy full SHA for 9fd797d

• separate exists and type_tcexp proof

  Gordon-Sau

  committed
  e0912f2

  Copy full SHA for e0912f2

Commits on Jun 25, 2024

• more cases

  Gordon-Sau

  committed
  41641fb

  Copy full SHA for 41641fb

Commits on Jun 27, 2024

• change PrimSeq rule

  Gordon-Sau

  committed
  b66f66d

  Copy full SHA for b66f66d

Commits on Jun 29, 2024

• change the defintion of destruactalbe_type and tcexp_exhaustive_cepat such that exhaustiveness preserves after appending type defintions

  Gordon-Sau

  committed
  e936710

  Copy full SHA for e936710

• Merge branch 'typeclassLang' of github.com:CakeML/pure into typeclassLang

  Gordon-Sau

  committed
  f941839

  Copy full SHA for f941839

Commits on Jun 30, 2024

• complete the induction theorem for dictionary translation

  Gordon-Sau

  committed
  5aed581

  Copy full SHA for 5aed581

Commits on Jul 8, 2024

• prove well-typedness of class_env_construct_dict

  Gordon-Sau

  committed
  6c5dfb4

  Copy full SHA for 6c5dfb4

Commits on Aug 20, 2024

• Merge branch 'master' into typeclassLang

  hrutvik

  committed
  79e3fed

  Copy full SHA for 79e3fed

Commits on Aug 27, 2024

• Add type class work to regression + top-level Holmakefile

  hrutvik

  committed
  86f5f1a

  Copy full SHA for 86f5f1a

Commits on Sep 6, 2024

• Merge branch 'typeclassLang' of github.com:CakeML/pure into typeclassLang

  Gordon-Sau

  committed
  a14f29c

  Copy full SHA for a14f29c

Commits on Sep 15, 2024

• typeclassLang: refactoring: updates the fintate maps to remove some side conditions and turns some tuples to records

  Gordon-Sau

  committed
  2cbd29b

  Copy full SHA for 2cbd29b

Commits on Sep 18, 2024

• typeclassLang: update typing Proof

  Gordon-Sau

  committed
  ee383ac

  Copy full SHA for ee383ac

• typeclassLang: update typing Proof

  Gordon-Sau

  committed
  c0e9c5e

  Copy full SHA for c0e9c5e

• typeclassLang: update the definition of type_elaborate_prog and prog_construct_dict

  Gordon-Sau

  committed
  cd168ee

  Copy full SHA for cd168ee

Commits on Sep 22, 2024

• typeclass: prove the superclass accessors in the translated lang is wel-typed

  Gordon-Sau

  committed
  d10134b

  Copy full SHA for d10134b

Commits on Sep 23, 2024

• typeclass: prove that the method accessors are well-typed and fix the distinctness condition for the variables in typeclasss_typing

  Gordon-Sau

  committed
  b47bb86

  Copy full SHA for b47bb86

Commits on Oct 1, 2024

• typeclass: prove impls well-typed and default implementations are well-typed

  Gordon-Sau

  committed
  be11591

  Copy full SHA for be11591

Commits on Oct 6, 2024

• update main theorem

  Gordon-Sau

  committed
  ec17734

  Copy full SHA for ec17734

Commits on Oct 8, 2024

• typeclass: complete typing translation proof

  Gordon-Sau

  committed
  e43ed9b

  Copy full SHA for e43ed9b

• typeclass: remove trailing whitespace

  Gordon-Sau

  committed
  d748f02

  Copy full SHA for d748f02

• typeclass: fix test_typeclass_typing

  Gordon-Sau

  committed
  9692a2d

  Copy full SHA for 9692a2d

Commits on Oct 10, 2024

• typeclass: fix typeclass_env_map_impl

  Gordon-Sau

  committed
  33f341f

  Copy full SHA for 33f341f

• typeclass: remove cycle_detection as it is now in HOL

  Gordon-Sau

  committed
  614c35c

  Copy full SHA for 614c35c

Commits on Oct 11, 2024

• typeclass: fix ast_to_cexp and fix texp_wf

  Gordon-Sau

  committed
  beaad40

  Copy full SHA for beaad40

• typeclass: small cleanup

  Gordon-Sau

  committed
  43fcd63

  Copy full SHA for 43fcd63

Commits on Oct 12, 2024

• typeclass: update destruct_type_cons

  Gordon-Sau

  committed
  7ec1b34

  Copy full SHA for 7ec1b34

Commits on Oct 13, 2024

• typeclass: update definition of exhaustive_cepat

  Gordon-Sau

  committed
  0bf0a37

  Copy full SHA for 0bf0a37

• typeclass: fix exhaustive_cepat

  Gordon-Sau

  committed
  daaf2a6

  Copy full SHA for daaf2a6

• typeclass: fix type_soundness_next

  Gordon-Sau

  committed
  5f8e72d

  Copy full SHA for 5f8e72d

Commits on Oct 14, 2024

• typeclass: fix type_soundness_up_to Case

  Gordon-Sau

  committed
  a7e79fb

  Copy full SHA for a7e79fb

Commits on Oct 16, 2024

• typeclass: fix the file structure. Revert changes in typing/ and move pure_tcexp and pure_tcexp_lemmas to typeclass/typing/, and remove the files that are not updated in typeclass/, and move typecl…

  Show description for 186f8ca
  Gordon-Sau

  committed
  186f8ca

  Copy full SHA for 186f8ca

• typeclass: add a readme

  Gordon-Sau

  committed
  8a5541a

  Copy full SHA for 8a5541a

• typeclass: add description for test_typeclass_typing

  Gordon-Sau

  committed
  af1b574

  Copy full SHA for af1b574

• typeclass: fix the workflow to build things in typeclass/

  Gordon-Sau

  committed
  bcd4189

  Copy full SHA for bcd4189

Commits on Dec 28, 2024

• Merge remote-tracking branch 'origin/master' into typeclassLang

  hrutvik

  committed
  5e43edd

  Copy full SHA for 5e43edd

Commits on Dec 29, 2024

• Merge remote-tracking branch 'origin/master' into typeclassLang

  hrutvik

  committed
  886a630

  Copy full SHA for 886a630

• Updates for CakeML/cakeml#1076

  hrutvik

  committed
  37e451c

  Copy full SHA for 37e451c