def by_rounds

stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:216

import Base

216def by_rounds(~Property: Nat -> Type,
217  ~few: @+count: Nat -> {Nat.is_lt(count,8n) == True{} : Bool} -> Property(count),
218  ~more: @+rest: Nat -> Property(rest) -> Property(8n+rest),count: Nat) -> Property(count):
219  match count:
220    case 0n: few(0n,{==})
221    case 1n: few(1n,{==})
222    case 2n: few(2n,{==})
223    case 3n: few(3n,{==})
224    case 4n: few(4n,{==})
225    case 5n: few(5n,{==})
226    case 6n: few(6n,{==})
227    case 7n: few(7n,{==})
228    case 1n+1n+1n+1n+1n+1n+1n+1n+ +rest:
229      more(rest,by_rounds(~Property,~few,~more,rest))