Skip to content

remove opt_rel_def in flat_to_closProofTheory #1247

New issue
New issue
Open
#1289
Open
remove opt_rel_def in flat_to_closProofTheory#1247
#1289
Assignees
xrchz
Labels
good first issuerefactoring
@ordinarymath

Description

@ordinarymath
ordinarymath
opened on Oct 2, 2025

cakeml/compiler/backend/proofs/flat_to_closProofScript.sml

Lines 72 to 76 in 6ddaf6f

Definition opt_rel_def[simp]:
opt_rel f NONE NONE = T /\
opt_rel f (SOME x) (SOME y) = f x y /\
opt_rel f _ _ = F
End

OPTREL should be used instead.

Metadata

Metadata

Assignees

Labels

good first issuerefactoring

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions