lean2/tests/lean/run/empty_eq.lean

open nat

inductive fin : nat → Type :=
| fz : Π n, fin (succ n)
| fs : Π {n}, fin n → fin (succ n)

open fin

definition case0 {C : fin zero → Type} : Π (f : fin zero), C f
| [none]


print definition case0
feat(frontends/lean/decl_cmds): allow 'empty' set of pattern matching equations 2015-03-05 22:34:56 +00:00			`open nat`
refactor(library/data): replace 'fin' with Haitao's 'less_than' The commit also fixes vector to use the new definition. 2015-06-05 17:32:24 +00:00
			`inductive fin : nat → Type :=`
			`\| fz : Π n, fin (succ n)`
			`\| fs : Π {n}, fin n → fin (succ n)`

feat(frontends/lean/decl_cmds): allow 'empty' set of pattern matching equations 2015-03-05 22:34:56 +00:00			`open fin`

			`definition case0 {C : fin zero → Type} : Π (f : fin zero), C f`
			`\| [none]`


			`print definition case0`