lambdapi icon indicating copy to clipboard operation
lambdapi copied to clipboard

Induction command does not work on vectors

Open fblanqui opened this issue 4 months ago • 0 comments

require open Stdlib.Set Stdlib.Prop Stdlib.Nat Stdlib.List;

symbol A:TYPE;

inductive V:ℕ → TYPE ≔ Vnil:V 0 | Vcons (x:A) n (v:V n):V(n +1);

symbol sample_2 n (v : V n) : π ⊤ ≔
begin
  induction and assume n; induction fail

fblanqui avatar Oct 10 '24 16:10 fblanqui