Map

📁 Source: MRiscX/AbstractSyntax/Map.lean

Statistics

Metric	Count
Definitions PMap, get, getKeys, getKeysAux, TMap, get, getKeys, getKeysAux, getLastKey, getValues, getValuesAux, instInhabitedPMap, default, instInhabitedTMap, default, instReprPMap, repr, instReprTMap, repr, «term(_↦_;_)»»), «termP(_↦_;_)»»)	21
Theorems p_update_eq, p_update_neq, t_update_eq, t_update_neq	4
Total	25

PMap

Definitions

Name	Category	Theorems
get 📖	CompOp	3 math math: p_update_neq, p_update_eq, MState.get_label_from_code
getKeys 📖	CompOp	—
getKeysAux 📖	CompOp	—

TMap

Definitions

Name	Category	Theorems
get 📖	CompOp	11 math math: MState.currInstruction_unfold, t_update_neq, MState.get_register_only_memory, MState.runNSteps_currInstruction, t_update_eq, MState.getRegisterAt_def, MState.TMap_register_le_zero_eq_zero, MState.setPc_getRegisterAt_def_indep, MState.get_register_only_register, MState.setPc_getMemoryAt_def_indep, MState.getMemoryAt_def
getKeys 📖	CompOp	—
getKeysAux 📖	CompOp	—
getLastKey 📖	CompOp	—
getValues 📖	CompOp	—
getValuesAux 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
PMap 📖	CompData	—
TMap 📖	CompData	—
instInhabitedPMap 📖	CompOp	—
instInhabitedTMap 📖	CompOp	—
instReprPMap 📖	CompOp	—
instReprTMap 📖	CompOp	—
«term(_↦_;_)» 📖» "API Documentation")	CompOp	—
«termP(_↦_;_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
p_update_eq 📖	mathematical	—	PMap.get PMap.put	—	PMap.get.eq_def
p_update_neq 📖	mathematical	—	PMap.get PMap.put	—	PMap.get.eq_def
t_update_eq 📖	mathematical	—	TMap.get TMap.put	—	TMap.get.eq_def
t_update_neq 📖	mathematical	—	TMap.get TMap.put	—	TMap.get.eq_def

instInhabitedPMap

Definitions

Name	Category	Theorems
default 📖	CompOp	—

instInhabitedTMap

Definitions

Name	Category	Theorems
default 📖	CompOp	—

instReprPMap

Definitions

Name	Category	Theorems
repr 📖	CompOp	—

instReprTMap

Definitions

Name	Category	Theorems
repr 📖	CompOp	—

---

← Back to Index