CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-20 08:47:14 +03:00
Code Issues Projects Releases Wiki Activity
807 Commits 41 Branches 8 Tags 60 MiB
383347bf00
Commit Graph

807 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Denis Merigoux
0259573cd0 Renamed files and makefiles fixes 2021-02-28 18:18:01 +01:00
Denis Merigoux
88d8dd3c31 Generalized plugin scheme for pygments 2021-02-28 18:10:41 +01:00
Denis Merigoux
d28323ae2e Timing information for debug 2021-02-28 11:15:18 +01:00
Jonathan Protzenko
3bcf85bd94 Missing files 2021-02-24 10:55:18 -07:00
Jonathan Protzenko
b206b7a93b For EN syntax highlighting, use a pygments plugin rather than a fork of pygments 2021-02-23 07:53:39 -07:00
Denis Merigoux
892b6daeee Most admits concern LCalc stepping + 1 assume for semantics of process_exceptions compared to empty_count 2021-02-22 01:18:05 +01:00
Denis Merigoux
ad54dfe691 Added dumb invariance lemma 2021-02-22 00:30:03 +01:00
Denis Merigoux
1071f3232d Proof went until the end, now havee to remove admits 2021-02-21 23:55:01 +01:00
Denis Merigoux
b2d9407c2b Fixed error and some mixup 2021-02-21 20:56:15 +01:00
Denis Merigoux
f14235fa5e All values case done 2021-02-21 20:23:13 +01:00
Denis Merigoux
80f2dffe1d Yet another proof case 2021-02-21 19:17:51 +01:00
Denis Merigoux
038c5b3e07 Proven one more subcase 2021-02-21 18:51:36 +01:00
Denis Merigoux
4efccbb335 Found theorem for all exceptions values 2021-02-21 17:24:52 +01:00
Denis Merigoux
6c881f7afb Code refactor 2021-02-21 16:38:52 +01:00
Denis Merigoux
ed4f589acb Proof structure of exceptions stepping case done 2021-02-21 16:15:17 +01:00
Denis Merigoux
c686b77b1d Proven case where tail steps to error 2021-02-21 15:27:33 +01:00
Denis Merigoux
8d5aa8e86e Split big theroem to manage it 2021-02-21 14:58:37 +01:00
Denis Merigoux
94b1c348d6 Weakened theorem to ensure good recursion 2021-02-21 14:38:11 +01:00
Denis Merigoux
38f7b72604 Restored proof again 2021-02-21 14:27:10 +01:00
Denis Merigoux
dbc8133821 Found correct version of exception stepping theorem 2021-02-21 13:24:27 +01:00
Denis Merigoux
68c36b26a1 Making slow progress 2021-02-21 00:36:06 +01:00
Denis Merigoux
e926adf6f0 Added thunk to ease proof of substitution correctness 2021-02-20 22:38:10 +01:00
Denis Merigoux
2efdd71866 Restored the proof somewhat 2021-02-20 20:31:51 +01:00
Denis Merigoux
b3fd1c030a proof of typing_empty_can_be_extended 2021-02-20 11:41:48 +01:00
Denis Merigoux
5b92165867 Restored type safety of lambda calculus 2021-02-19 22:06:09 +01:00
Denis Merigoux
9b4466b836 Type safety of default calculus restoed 2021-02-19 19:01:23 +01:00
Denis Merigoux
6662a07bfd Making progress on default calculus 2021-02-19 15:09:39 +01:00
Denis Merigoux
21cf048a19 Starting transition to De Bruijn 2021-02-19 14:01:27 +01:00
Denis Merigoux
fb63c8afc8 Restore tests 2021-02-19 09:09:13 +01:00
Denis Merigoux
e9b134ab79 Progress on section121 after pair programming session 2021-02-18 18:18:34 +01:00
Denis Merigoux
cfd2a4bcc3 WIP 2021-02-18 16:12:23 +01:00
Denis Merigoux
c2dc8db6ac Fix list stepping semantics in both default and lambda calculus 2021-02-17 16:24:19 +01:00
Denis Merigoux
f5caa5d5fb Merge branch 'master' into certfication_proof 2021-02-17 15:32:38 +01:00
Denis Merigoux
daeb50212b
Merge pull request #77 from AltGr/gen-parser-msgs 
Generate parser.messages from dune
 2021-02-17 11:04:19 +01:00
Denis Merigoux
ea451bc46f Add rule to recreate the error message file from scratch 2021-02-17 10:57:48 +01:00
Denis Merigoux
716700c8be Merge branch 'master' into gen-parser-msgs 2021-02-17 10:45:43 +01:00
Denis Merigoux
da828a5304
Merge pull request #76 from AltGr/mlis 
Add .mlis for all of Catala
 2021-02-17 10:41:31 +01:00
Denis Merigoux
44a937630d Removed duplicate comments 2021-02-17 10:34:47 +01:00
Denis Merigoux
f70a4af7b4 More general theorem, second difficult case OK 2021-02-16 16:20:42 +01:00
Denis Merigoux
ddfc67af55 Prove small precedes lemma 2021-02-15 22:01:37 +01:00
Denis Merigoux
252748968a Fix name 2021-02-15 21:45:11 +01:00
Denis Merigoux
494ba820b0 Continue Section121 2021-02-15 21:41:31 +01:00
Denis Merigoux
35ae5ff39a Flesh out other case; more general theorem needed 2021-02-15 20:06:33 +01:00
Denis Merigoux
7711cad2f4 First case fully proven 2021-02-15 16:18:20 +01:00
Denis Merigoux
d7cfbb2eba First case of difficult translation proven 2021-02-15 14:18:55 +01:00
Denis Merigoux
9ffb0c134e Proved one complicated lift 2021-02-15 11:35:51 +01:00
Denis Merigoux
adf16489bf Back to simpler version of step commute 2021-02-14 23:25:29 +01:00
Denis Merigoux
e3e3896d0a Some progress 2021-02-14 22:47:40 +01:00
Denis Merigoux
3776362c67 More interface cleaning 2021-02-14 12:01:32 +01:00
Denis Merigoux
220169aea1 Clean surface mlis 2021-02-14 11:50:05 +01:00