matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Mon, 30 Apr 2018 16:12:14 +0000 (18:12 +0200)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Mon, 30 Apr 2018 16:12:14 +0000 (18:12 +0200)
commit	5a0d5df90ad4096c4d7bdc50ce69cf8673ea6e57
tree	96deb979c180f40aee31bb239f75cb75d552b5b7	tree \| snapshot
parent	f129bbbfda0e65a5f92ec086246f6e288376d4f9	commit \| diff

initial definition of λδ model

+ intensional and extensional variant
+ denotational equivalence

this is previously uncommitted matter ported to current version of λδ

14 files changed:

.gitignore		diff \| blob \| history
matita/matita/contribs/lambdadelta/apps_2/models/deq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/models/model.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/models/model_push.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/models/veq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/notation/models/at_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/notation/models/inwbrackets_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/apps_2/notation/models/wbrackets_4.ma	[new file with mode: 0644]	blob
matita/matita/predefined_virtuals.ml		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom