leanprover-community/mathlib

Pull Requests Commits

rewrite fsum for the purpose of configurations

MadPidgeon committed 5 years ago

3863794d

Move fsum to separate file, finaly type-checks

MadPidgeon committed 5 years ago

c70740c5

Merge remote-tracking branch 'origin/computability-list' into computability-compositions

pimsp committed 5 years ago

856dac63

Added proof that taking a step increases a stack size by at most the function length

pimsp committed 5 years ago

6d98ae04

Added finiteness condition and fixed remarks from Mario

pimsp committed 5 years ago

86bd525c

Put everything in turing namespace

pimsp committed 5 years ago

138e8cce

Fixed comments by Mario + cleaned up what's happening in namespace fin_tm2

pimsp committed 5 years ago

dc0c36ea

Merge branch 'computability-list' of https://github.com/leanprover-community/mathlib into computability-list

pimsp committed 5 years ago

613235f1

Fixed corrections by Rob

pimsp committed 5 years ago

3c4b1522

Clean up proofs + define length of statement

pimsp committed 5 years ago

246f8d57

Merge branch 'master' into computability-list

robertylewis committed 5 years ago

Verified 860c6c83

Merge remote-tracking branch 'origin/computability-list' into computability-compositions

pimsp committed 5 years ago

a03e1f09

Merge branch 'computability-compositions' of https://github.com/leanprover-community/mathlib into computability-compositions

MadPidgeon committed 5 years ago

285b0e72

Almost defined composition of TM

MadPidgeon committed 5 years ago

17f0c1ed

feat(data/mv_polynomial): fill in API for vars (#4018)

robertylewis committed 5 years ago

62963861

chore(data/finset/lattice): remove unneeded assumptions (#4020)

jcommelin committed 5 years ago

7b3c653b

First (ugly) proof of (size increase stack) \leq (length of statementt)

pimsp committed 5 years ago

43a4f23d

feat(computability/encoding): define encoding of basic data types (#3976)

MadPidgeon committed 5 years ago

815a2f97

Merge branch 'computability-list' of https://github.com/leanprover-community/mathlib into computability-list

MadPidgeon committed 5 years ago

6746e8bb

(Final Pre-PR commit) Add inhabited instances

MadPidgeon committed 5 years ago

335a0080

Removed unnecessary file

pimsp committed 5 years ago

92da9cb0

Remove previously named file

pimsp committed 5 years ago

23b1e0b9

Merge remote-tracking branch 'origin/computability-list' into computability-compositions

pimsp committed 5 years ago

c8023274

pimsp committed 5 years ago

9b249a51

Delete old structures

MadPidgeon committed 5 years ago

0a684544

Merge branch 'computability' into computability-list

pimsp committed 5 years ago

b96f8658

Fixed remarks Mario (except making Gamma a parameter - see github)

pimsp committed 5 years ago

3c43dd42

feat(linear_algebra/char_poly): rephrase Cayley-Hamilton with `aeval', define `matrix.min_poly` (#4040)

awainverse committed 5 years ago

364d5d4c

Changed encodek to decode_encode and removed superfluous parentheses

pimsp committed 5 years ago

cf222d2b

Fix typo in docstring

pimsp committed 5 years ago

Verified 4ae74bbd

Older