matita.cs.unibo.it Git - fireball-separation.git/commit

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

projects / fireball-separation.git / commit

author	acondolu <andrea.condoluci@unibo.it>
	Tue, 25 Jul 2017 15:16:57 +0000 (17:16 +0200)
committer	acondolu <andrea.condoluci@unibo.it>
	Tue, 25 Jul 2017 15:16:57 +0000 (17:16 +0200)
commit	6d9e673e3a6896f487988d897f927d07104d6a73
tree	19287118ff9d25e49597a73c6e39fe2d9023c106	tree \| snapshot
parent	d787e6e7880a454ce6a2dba80a554c93e0eeab41	commit \| diff

Code for critical eat reimplemented

x is now critical eat iff it is the head of a num and it occurs unprotected
in other numbers or in divergent terms where unprotected means
- as the scrutinee of a match, with wrong arity
- everywhere else with too great arity

The new definition fixes problems/bugs2 (renamed to problems/bomb)

ocaml/lambda4.ml		diff \| blob \| history
ocaml/problems/bomb	[new file with mode: 0644]	blob
ocaml/problems/bugs2	[deleted file]	blob \| history
ocaml/problems/q		diff \| blob \| history
ocaml/util.ml		diff \| blob \| history
ocaml/util.mli		diff \| blob \| history

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

RSS Atom