Repository navigation
Expand file tree
/
Copy pathDemos.lean
More file actions
82 lines (82 loc) · 2.55 KB
/
Copy pathDemos.lean
File metadata and controls
82 lines (82 loc) · 2.55 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
import Demos.Clob.Cases
import Demos.Clob.Module
import Demos.Clob.Program
import Demos.Clob.Verify
import Demos.Drone.Acceleration
import Demos.Drone.Cases
import Demos.Drone.Correct
import Demos.Drone.Corridor
import Demos.Drone.Flat
import Demos.Drone.Forward
import Demos.Drone.Gluing
import Demos.Drone.Kinematics
import Demos.Drone.Module
import Demos.Drone.Motion
import Demos.Drone.Planner
import Demos.Drone.Program
import Demos.Drone.Safety
import Demos.Drone.Timing
import Demos.Drone.Total
import Demos.Drone.Trajectory
import Demos.Drone.Verify
import Demos.Drone.WholeFlight
import Demos.Euler.Balance
import Demos.Euler.Cases
import Demos.Euler.Cfl
import Demos.Euler.Enclosure
import Demos.Euler.Equations.CharacteristicSpeed
import Demos.Euler.Equations.Eigenbasis
import Demos.Euler.Equations.Eigenvectors
import Demos.Euler.Equations.Flux
import Demos.Euler.Equations.Hyperbolicity
import Demos.Euler.Equations.Jacobian
import Demos.Euler.Equations.LaxFriedrichs
import Demos.Euler.Equations.LeftEigenvectors
import Demos.Euler.Equations.Minmod
import Demos.Euler.Equations.ReconstructionCounterexample
import Demos.Euler.Equations.Rotation
import Demos.Euler.Equations.Rusanov
import Demos.Euler.FirstOrderBalance
import Demos.Euler.Hyperbolic
import Demos.Euler.Module
import Demos.Euler.RealState
import Demos.Euler.ReconstructedBalance
import Demos.Euler.ReconstructionAccuracy
import Demos.Euler.Reference.Accepted
import Demos.Euler.Reference.Boundary
import Demos.Euler.Reference.Component
import Demos.Euler.Reference.Constants
import Demos.Euler.Reference.FluxTerms
import Demos.Euler.Reference.Interface
import Demos.Euler.Reference.Internal
import Demos.Euler.Reference.InternalGuard
import Demos.Euler.Reference.Pressure
import Demos.Euler.Reference.PressureReference
import Demos.Euler.Reference.Radicand
import Demos.Euler.Reference.Side
import Demos.Euler.Reference.Sound
import Demos.Euler.Reference.SoundRatio
import Demos.Euler.Reference.Speed
import Demos.Euler.Reference.Transport
import Demos.Euler.Reference.Update
import Demos.Euler.SpeedCounterexample
import Demos.Euler.Total
import Demos.Euler.Verify
import Demos.Euler.Words
import Demos.Gpt.Bytes
import Demos.Gpt.Causal
import Demos.Gpt.Composites
import Demos.Gpt.Exact
import Demos.Gpt.Generation
import Demos.Gpt.Module
import Demos.Gpt.SampleVerify
import Demos.Gpt.StepVerify
import Demos.Gpt.Verify
import Demos.Gpt32.Compose
import Demos.Gpt32.Driver
import Demos.Gpt32.Exec
import Demos.Gpt32.HostProgram
import Demos.Gpt32.Kernels
import Demos.Gpt32.Module
import Demos.Gpt32.Proofs
import Demos.Gpt32.Specs