summaryrefslogtreecommitdiff
path: root/src/Helium/Semantics/Denotational.agda
AgeCommit message (Expand)Author
2022-01-07Rename ⟦_⟧ to float.Greg Brown
2021-12-28Make the denotational semantics total.Greg Brown
2021-12-27Introduce Everything.agda to aid in overall compilation.Greg Brown
2021-12-21Define execBeats, a wrapper to execute beat-wise instructions.Greg Brown
2021-12-21Define semantics of vqdmulh.Greg Brown
2021-12-21Define semantics for vmulh.Greg Brown
2021-12-20Define vsub.Greg Brown
2021-12-20Remove bitstring addition.Greg Brown
2021-12-20Extract structures shared by most binary vector operations.Greg Brown
2021-12-20Define vmul.Greg Brown
2021-12-20Inline and rearrange to make vadd and vhsub look more similar.Greg Brown
2021-12-20Define semantics of vhsub.Greg Brown
2021-12-20Improve type-checking efficiency.Greg Brown
2021-12-20Define semantics for vadd.Greg Brown