]> matita.cs.unibo.it Git - helm.git/commit
new calculation of recursive parameters in guarded by destructors:
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 17 Apr 2008 16:12:12 +0000 (16:12 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 17 Apr 2008 16:12:12 +0000 (16:12 +0000)
commit97b18234921aec71a8b89ec2c1b058e12e5e043c
tree5c8e77ba6a0f2a0fcc7dacb8c4122606bf8d9360
parent998a7855d00bcb55525a82138a3bfb4183d99014
new calculation of recursive parameters in guarded by destructors:

  inductive I : Type :=
  | K : list (pair Type I) -> I

  let rec f t on t : I -> bool :=
  match t with
  | k ((nat, x)::_) -> f x
  | k _ -> true

is now accepted. the arg of k used to be recursive but not the head of the list
(only its tail) since constructors types were not specialized on actual left
arguments (and the information that the type of the head contains I was lost).
helm/software/components/cic_proof_checking/cicTypeChecker.ml
helm/software/components/cic_proof_checking/cicTypeChecker.mli
helm/software/components/cic_unification/cicRefine.ml