Code

Compile records#22

Code

Open

lemastero wants to merge 3 commits intomasterlemastero/agda2rust:masterfrom record-typeslemastero/agda2rust:record-typesCopy head branch name to clipboard

+65-26

Commits

Commits on Dec 19, 2023

• compile record name

  

  lemastero

  committed
  f42ebab

  Copy full SHA for f42ebab

Commits on Apr 30, 2024

• compile record elements

  lemastero

  committed
  87fa0c7

  Copy full SHA for 87fa0c7

• compile record elements - cleanup imports

  lemastero

  committed
  3c0f18d

  Copy full SHA for 3c0f18d