Skip to content

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

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 #2334

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

copyright-header.yml

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