hsk · April 27, 2026 01:04
diff --git a/den.agda b/den.agda
 module den where
 open import Data.Nat
 open import Data.Nat.Properties
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)

 data Expr : Set where
  Lit : ℕ → Expr
  _x_ : Expr → Expr → Expr

 -- 表示的意味論（denotation）
 [[_]] : Expr → ℕ
 [[ Lit n ]]   = n
 [[ e1 x e2 ]] = [[ e1 ]] * [[ e2 ]]

 -- 例
 example : [[ Lit 3 x Lit 2 ]] ≡ [[ Lit 2 x Lit 3 ]]
 example = refl
	module den where
	open import Data.Nat
	open import Data.Nat.Properties
	open import Relation.Binary.PropositionalEquality using (_≡_; refl)

	data Expr : Set where
	Lit : ℕ → Expr
	_x_ : Expr → Expr → Expr

	-- 表示的意味論（denotation）
	[[_]] : Expr → ℕ
	[[ Lit n ]] = n
	[[ e1 x e2 ]] = [[ e1 ]] * [[ e2 ]]

	-- 例
	example : [[ Lit 3 x Lit 2 ]] ≡ [[ Lit 2 x Lit 3 ]]
	example = refl
No results found