]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5acff80) | patch
example:
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 17 Apr 2008 16:55:36 +0000 (16:55 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 17 Apr 2008 16:55:36 +0000 (16:55 +0000)
commit6ebe894ff0fee5d99bad615ce053128292657dee
tree5a022c4be556ad3f08f34715fa0f49f2ee55f53ftree | snapshot
parent5acff80c93b3e3df4a52ff8cb9596de46f7bd924commit | diff
example:
  inductive I : Type :=
  | k : \forall A. (A -> I)-> I

  match t with
  | k _ f => f w (* is smaller than t even if applied! *)
helm/software/components/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.