]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b499647) | patch
Code for computing patterns the way Haskell likes them (lhs + rhs).
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Aug 2012 16:26:15 +0000 (16:26 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Aug 2012 16:26:15 +0000 (16:26 +0000)
commitefdc4b8deed29fbcd4b2673e1f174696cd4c67d6
tree890075e7762cbf74fda91434a2482dff12921625tree | snapshot
parentb4996474adbb67dda2e40b2bbcc727807fb48a1ccommit | diff
Code for computing patterns the way Haskell likes them (lhs + rhs).
Currently bugged:
 - some DeBrujin problems in the rhs
 - ignores the extracted type of the constructor (uses the CiC type)
 - does not perform eta-expansion when needed
matita/components/ng_kernel/nCicExtraction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.