NPAへ戻る
Module
Mathlib.Core.Reduction
npa-mathlib
Packages
2
Module
63
Theorem
750
Declarations
1016
信頼境界外の sidecar
Source text や表示 overlay は提示用メタデータです。信頼する証拠は署名済み証明書と checker の結果です。
Theorem
5
Definition
1
Inductive type
0
Axiom
0
Declarations
Hashes
- source
- sha256:53f6a264f4626ff04d6c5de4d5537e3788ea03b28c0c507c8137de1c55fbf531
- certificateFile
- sha256:df9ac4f4d242d488d044e5dc51b6c78402e921531d6e8d4b625257873d8d6332
- export
- sha256:2569ced477b19ec5058860d727cf520416e353f6fe8c682a323a605869ae7902
- axiomReport
- sha256:70b2d0f35f9ebfff46bdf399b80487f0c76ffd6460ab930f733af1f889d2fc65
- certificate
- sha256:a30a2ceacf391a9635367aa4f760ccf60431809c27f973035d0ed1dede98fd22
Source
import Std.Nat.Basic
def reduction_id_nat :
forall (n : Nat), Nat :=
fun n => n
theorem beta_id_nat :
forall (n : Nat), Nat :=
fun n => (fun (x : Nat) => x) n
theorem beta_const_nat :
forall (n : Nat), forall (m : Nat), Nat :=
fun n => fun m => (fun (x : Nat) => fun (y : Nat) => x) n m
theorem let_id_nat :
forall (n : Nat), Nat :=
fun n => let x : Nat := n in x
theorem let_const_nat :
forall (n : Nat), Nat :=
fun n => let z : Nat := Nat.zero in z
theorem delta_id_nat :
forall (n : Nat), Nat :=
reduction_id_nat