Skip to content

chore: unify String.csize : Nat and Char.utf8Size : UInt32 as Char.size : Nat #2335

chore: unify String.csize : Nat and Char.utf8Size : UInt32 as Char.size : Nat

chore: unify String.csize : Nat and Char.utf8Size : UInt32 as Char.size : Nat #2335

Triggered via pull request June 10, 2024 23:52
@kim-emkim-em
synchronize #4357
Char.size
Status Success
Total duration 27s
Artifacts

copyright-header.yml

on: pull_request
check-lean-files
16s
check-lean-files
Fit to window
Zoom out
Zoom in