Merging devel #3

g-nakov · 2024-09-09T16:07:14Z

Getting up to speed.

…position

…sed)

…code; add option for hiding generated code

g-nakov added 30 commits May 30, 2023 12:27

[ new ] parsing typechecking and type synth dirs

f4b3492

[ new ] parsing type declarations and type expressions

8e56540

[ new ] terms and substitutions

943a1ed

[ new ] showing terms; smart cons

0b162ec

[ new ] cdb subst; int atoms

94a9bb9

[ new ] coreTT

d41a834

[ new ] typechecking and evaluating integers

2a8b7d5

[ new ] normal forms over arbitrary set of gens

cd95add

[ new ] typechecking and eval Enum types

efad423

[ cleanup ]

4a7ff24

[ new ] testing infrastructure

bf96580

[ new ] neutral terms in Enums.

3242806

[ test ] missing golden values

9b36326

[ test ] testing infrastructure

cfe9e09

[ fix ] remove obsolete example

ab3d40a

[ new ] Pi and Sigma types (wip)

e0009b5

[ new ] computation is in TC

2d53c59

[ broken ] evalSynth; problems with pairing

77afec7

[ new ] sort indexed terms

d0ec28e

[ new ] terms indexed by sort

7ce5b6e

[ new ] compiling and previous tests passing

9cabbc6

[ fix ] evalSynth

aa6945b

[ new ] evalSynth; fixes

9b9342b

[ new ] stab at eta-expansion

1188634

[ fix ] eval atoms

7a71374

[ testing ] fix and move tests from CoreTT

8d3e4a7

[ new ] transport implemented

796eb04

[ new ] more subtyping

0683d91

[ new ] typechecking matrices - single, horizontal and vertical juxta…

a0a97b7

…position

[ new ] added matrix diagram

c7e9be1

fredrikNordvallForsberg and others added 29 commits August 15, 2024 12:06

[ example ] remove punchline

0f52ec5

[ writing ] imeko2024 presentation

3e861f4

more aggressively infer type of string literals

f994e9a

[ IMEKO WC 2024 ] polish slides

52efdb1

[ IMEKO WC 2024 ] slide numbers

fb15d1e

[ IMEKO WC 2024 ] more polishing of slides

417623e

[ progress ] more constraint solving

e9c6c33

[ more ] structural subtyping

2c19d35

[ progress ] more matrices can be multiplied

04a528f

[ progress ] division

689aad4

[ emacs ] load hideshow mode (but don't fold by default; to be discus…

56d30b2

…sed)

[ new ] beginning of group theory work

27b45d1

[ wip ] matrix multiplication with quantities

0589516

[ new ] infer synth mode in assignment

24e1ab3

[ new ] combine dimensions with standard units

e1f8b1d

[ minor ] rearrange diagnostics to work better with hiding generated …

c78bfec

…code; add option for hiding generated code

[ refactor ] move normalisation of constraint fields to updateConstraint

51deb2b

[ new ] fix for constant cell elaboration; beginning of addition

19bb4bc

[ progress ] wiggle room injected into addition

8134699

[ examples ] matrixadd examples

e472e1e

[ cleaning ] remove some labmate output

6f7e82c

[ printing ] some nicer prettyprinting of matrices

dcc9daa

[ fix ] missing space in output

56023df

[ broken ] matrix transposition

d4e6397

[ fix ] restore old functionality with new FlexEh

2e389b0

[ progress ] made flexEh check for permutations of fresh variables

ceb121d

[ pprint ] slightly better /

cbe489a

[ print ] pretty printing for Quantity

24cb6c6

[ new ] support for subtraction

52ab8f3

g-nakov merged commit 5c0724d into main Sep 9, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Merging devel #3

Merging devel #3

g-nakov commented Sep 9, 2024

Merging devel #3

Merging devel #3

Conversation

g-nakov commented Sep 9, 2024