{"push_id":581399262,"size":1,"distinct_size":1,"ref":"refs/heads/master","head":"da2d0c2614e4f08f8b1bfbc9c25ce2b9c22803c8","before":"f83a53af5d39d3cf2fc4879912943467e3d9402d","commits":[{"sha":"da2d0c2614e4f08f8b1bfbc9c25ce2b9c22803c8","author":{"email":"e5dde5c9b235fcbea83b849d5bf49002b5ae0399@gmail.com","name":"Ting-Yen Lai"},"message":"    tailₙ-suc : ∀ {n A} → (xs : RandomAccessList A n) → (p : False (null? xs))\n              → suc ⟦ tailₙ xs p ⟧ₙ ≡ ⟦ xs ⟧ₙ\n    tail-suc : ∀ {A} → (xs : RandomAccessList A 0) → (p : False (null? xs))\n             → suc ⟦ tail xs p ⟧ ≡ ⟦ xs ⟧","distinct":true,"url":"https://api.github.com/repos/banacorn/numericalrepresentation/commits/da2d0c2614e4f08f8b1bfbc9c25ce2b9c22803c8"}]}