Bedrock
English · 中文
模块
  • Example.Doubling
  • Example.Naturals
  • HelloWorld

Hello, World

Bedrock 的最小文学化模块:自反性给出从任意一点到其自身的道路,由构建本站点的同一套工具链检查。

{-# OPTIONS --cubical --safe --guardedness #-}
module HelloWorld where

open import Cubical.Foundations.Prelude

hello : {ℓ : Level} {A : Type ℓ} (x : A) → x ≡ x
hello x = refl
Rendered with a generator adapted from the 1lab (AGPL-3.0). · 源码
© 2026 choukh (choukyuhei@gmail.com) · 内容以 CC BY-NC-SA 4.0 许可