HEL/midas
1
0
Fork 0
Code Issues Pull Requests Releases Activity

User manual #23

Merged
HEL merged 11 commits from feat/manual into main 2026-06-30 14:11:45 +00:00
Conversation 0 Commits 11 Files Changed 4 +1137
HEL commented 2026-06-30 14:11:35 +00:00
Owner
Copy Link

This PR adds a user manual explaining how to use Midas, including the Midas language reference and supported Python syntax.
The last section listing available commands and their options is still to do but the rest is more or less complete

NB: The manual includes a .sublime-syntax definition file for the Midas language

This PR adds a user manual explaining how to use Midas, including the Midas language reference and supported Python syntax. The last section listing available commands and their options is still to do but the rest is more or less complete NB: The manual includes a `.sublime-syntax` definition file for the Midas language
HEL self-assigned this 2026-06-30 14:11:35 +00:00
HEL added 11 commits 2026-06-30 14:11:35 +00:00
docs: setup user manual 93ddb28802
feat(manual): complete introduction and quick start bd47d33355
feat(manual): add sublime syntax for Midas 386018b956
feat(manual): document type statement f9f3ade6c7
feat(manual): document predicate and constraints 4c39504750
feat(manual): document supported Python syntax 4b2b0fe476
feat(manual): wrap all code in figures 759b416bf3
feat(manual): add listings outline and tweak template 31e696c938
fix(manual): typos e28f324a85
fix(manual): end syntax highlighting of extend body e15607b763
feat(manual): add strings to midas syntax def 6a0401833c
HEL merged commit d582df5927 into main 2026-06-30 14:11:45 +00:00
HEL deleted branch feat/manual 2026-06-30 14:11:45 +00:00
Sign in to join this conversation.
Reviewers
No Reviewers
Labels
No items
No Label
Milestone
No items
No Milestone
Assignees
Clear assignees
HEL
No Assignees HEL
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: HEL/midas#23
Delete Branch "feat/manual"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?